src/Pure/more_thm.ML
changeset 33697 7d6793ce0a26
parent 33666 e49bfeb0d822
child 33713 5249bbca5fab
--- a/src/Pure/more_thm.ML	Sun Nov 15 15:14:02 2009 +0100
+++ b/src/Pure/more_thm.ML	Sun Nov 15 15:14:28 2009 +0100
@@ -279,9 +279,10 @@
 
 val forall_elim_vars = forall_elim_vars_aux Term.strip_all_vars;
 
-fun forall_elim_var i th = forall_elim_vars_aux
-  (fn Const ("all", _) $ Abs (a, T, _) => [(a, T)]
-  | _ => raise THM ("forall_elim_vars", i, [th])) i th;
+fun forall_elim_var i th =
+  forall_elim_vars_aux
+    (fn Const ("all", _) $ Abs (a, T, _) => [(a, T)]
+      | _ => raise THM ("forall_elim_vars", i, [th])) i th;
 
 end;