diff -r 8ff4a0ea49b2 -r ba7a7c56bed5 src/HOL/Tools/function_package/pattern_split.ML
--- 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
-
-
-
-
-
-
-
-
-
-