Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/goal.ML
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) =>
isabelle