1 files changed, 0 insertions, 35 deletions
diff --git a/sci-mathematics/isabelle/files/isabelle-2012-redundant-equations-in-function-definitions-error.patch b/sci-mathematics/isabelle/files/isabelle-2012-redundant-equations-in-function-definitions-error.patch
deleted file mode 100644
index 18ae43d00fe5..000000000000
--- a/sci-mathematics/isabelle/files/isabelle-2012-redundant-equations-in-function-definitions-error.patch
+++ /dev/null
@@ -1,35 +0,0 @@
-diff -r dd611ab202a8 -r e7e647949c95 src/HOL/Tools/Function/fun.ML
---- a/src/HOL/Tools/Function/fun.ML	Wed Jun 06 10:35:05 2012 +0200
-+++ b/src/HOL/Tools/Function/fun.ML	Wed Jun 06 21:36:21 2012 +0200
-@@ -84,10 +84,10 @@
-     spec @ mk_catchall fixes arity_of
-   end
- 
--fun warnings ctxt origs tss =
-+fun further_checks ctxt origs tss =
-   let
--    fun warn_redundant t =
--      warning ("Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t))
-+    fun fail_redundant t =
-+      error (cat_lines ["Equation is redundant (covered by preceding clauses):", Syntax.string_of_term ctxt t])
-     fun warn_missing strs =
-       warning (cat_lines ("Missing patterns in function definition:" :: strs))
- 
-@@ -100,7 +100,7 @@
-          @ ["(" ^ string_of_int (length rest) ^ " more)"])
- 
-     val _ = (origs ~~ tss')
--      |> map (fn (t, ts) => if null ts then warn_redundant t else ())
-+      |> map (fn (t, ts) => if null ts then fail_redundant t else ())
-   in
-     ()
-   end
-@@ -119,7 +119,7 @@
-       val compleqs = add_catchall ctxt fixes feqs (* Completion *)
- 
-       val spliteqs = Function_Split.split_all_equations ctxt compleqs
--        |> tap (warnings ctxt feqs)
-+        |> tap (further_checks ctxt feqs)
- 
-       fun restore_spec thms =
-         bnds ~~ take (length bnds) (unflat spliteqs thms)