tuned;
authorwenzelm
Mon Jun 04 21:04:20 2007 +0200 (2007-06-04)
changeset 232393648e97da60b
parent 23238 3de6e253efc4
child 23240 7077dc80a14b
tuned;
src/Pure/old_goals.ML
     1.1 --- a/src/Pure/old_goals.ML	Mon Jun 04 21:04:19 2007 +0200
     1.2 +++ b/src/Pure/old_goals.ML	Mon Jun 04 21:04:20 2007 +0200
     1.3 @@ -157,7 +157,7 @@
     1.4        val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg;
     1.5        val (As, B) = Logic.strip_horn horn;
     1.6        val atoms = atomic andalso
     1.7 -            forall (fn t => not (can Logic.dest_implies t orelse Logic.is_all t)) As;
     1.8 +            forall (fn t => not (can Logic.dest_implies t orelse can Logic.dest_all t)) As;
     1.9        val (As,B) = if atoms then ([],horn) else (As,B);
    1.10        val cAs = map (cterm_of thy) As;
    1.11        val prems = map (rewrite_rule rths o forall_elim_vars 0 o Thm.assume) cAs;