Logic.is_all;

--- a/src/Pure/conv.ML	Mon Jun 23 23:45:44 2008 +0200
+++ b/src/Pure/conv.ML	Mon Jun 23 23:45:45 2008 +0200
@@ -133,7 +133,7 @@
 
 (*rewrite B in !!x1 ... xn. B*)
 fun params_conv n cv ctxt ct =
-  if n <> 0 andalso can Logic.dest_all (Thm.term_of ct)
+  if n <> 0 andalso Logic.is_all (Thm.term_of ct)
   then arg_conv (abs_conv (params_conv (n - 1) cv o #2) ctxt) ct
   else cv ctxt ct;
 

--- a/src/Pure/old_goals.ML	Mon Jun 23 23:45:44 2008 +0200
+++ b/src/Pure/old_goals.ML	Mon Jun 23 23:45:45 2008 +0200
@@ -155,7 +155,7 @@
       val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg;
       val (As, B) = Logic.strip_horn horn;
       val atoms = atomic andalso
-            forall (fn t => not (can Logic.dest_implies t orelse can Logic.dest_all t)) As;
+            forall (fn t => not (can Logic.dest_implies t orelse Logic.is_all t)) As;
       val (As,B) = if atoms then ([],horn) else (As,B);
       val cAs = map (cterm_of thy) As;
       val prems = map (rewrite_rule rths o Thm.forall_elim_vars 0 o Thm.assume) cAs;