src/Pure/old_goals.ML

       val _ = warning "Obsolete goal command encountered";
       val {thy, t=horn,...} = rep_cterm chorn;
       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;
       val cB = cterm_of thy B;
       val st0 = let val st = Goal.init cB |> fold Thm.weaken cAs