changeset 56245 | 84fc7dfa3cd4 |
parent 55559 | d4aea4bbe87f |
child 58008 | aa72531f972f |
--- a/src/Pure/goal.ML Fri Mar 21 15:12:03 2014 +0100 +++ b/src/Pure/goal.ML Fri Mar 21 20:33:56 2014 +0100 @@ -327,8 +327,8 @@ (* non-atomic goal assumptions *) -fun non_atomic (Const ("==>", _) $ _ $ _) = true - | non_atomic (Const ("all", _) $ _) = true +fun non_atomic (Const ("Pure.imp", _) $ _ $ _) = true + | non_atomic (Const ("Pure.all", _) $ _) = true | non_atomic _ = false; fun assume_rule_tac ctxt = norm_hhf_tac ctxt THEN' CSUBGOAL (fn (goal, i) =>