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/Provers/clasimp.ML
changeset 8154 dab09e1ad594
parent 7957 0196b2302e21
child 8168 9d2ac5439089 
--- a/src/Provers/clasimp.ML	Fri Jan 28 12:10:47 2000 +0100
+++ b/src/Provers/clasimp.ML	Fri Jan 28 12:12:06 2000 +0100
@@ -158,7 +158,7 @@
   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_clasimpset ctxt));
 
 fun clasimp_meth' tac prems ctxt = Method.METHOD (fn facts =>
-  FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_clasimpset ctxt)));
+  FINDGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_clasimpset ctxt)));
 
 val clasimp_method = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth;
 val clasimp_method' = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth';
isabelle