# HG changeset patch # User wenzelm # Date 1180983860 -7200 # Node ID 3648e97da60bb8aa1f417016b2da6f4336f0acd4 # Parent 3de6e253efc4e408be28ed644176df3b7103654e tuned; 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;