diff -r 3de6e253efc4 -r 3648e97da60b src/Pure/old_goals.ML --- a/src/Pure/old_goals.ML Mon Jun 04 21:04:19 2007 +0200 +++ b/src/Pure/old_goals.ML Mon Jun 04 21:04:20 2007 +0200 @@ -157,7 +157,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 Logic.is_all t)) As; + forall (fn t => not (can Logic.dest_implies t orelse can Logic.dest_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 forall_elim_vars 0 o Thm.assume) cAs;