--- 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;