--- a/src/HOL/Tools/function_package/pattern_split.ML Wed Aug 02 22:26:40 2006 +0200
+++ b/src/HOL/Tools/function_package/pattern_split.ML Wed Aug 02 22:26:41 2006 +0200
@@ -11,8 +11,8 @@
signature FUNDEF_SPLIT =
sig
- val split_some_equations : ProofContext.context -> (('a * ('b * bool)) * Term.term) list
- -> (('a * 'b) * Term.term list) list
+ val split_some_equations :
+ Proof.context -> (('a * ('b * bool)) * term) list -> (('a * 'b) * term list) list
end
@@ -115,19 +115,4 @@
split_aux [] eqns
end
-
-
-
-
-
end
-
-
-
-
-
-
-
-
-
-