--- a/src/Pure/old_goals.ML Fri Oct 06 15:39:29 2006 +0200
+++ b/src/Pure/old_goals.ML Sat Oct 07 01:30:58 2006 +0200
@@ -156,7 +156,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(Logic.is_implies t orelse Logic.is_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 forall_elim_vars 0 o Thm.assume) cAs;