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/simplifier.ML
changeset 58957 c9e744ea8a38
parent 58048 aa6296d09e0e
child 58963 26bf09b95dda 
--- a/src/Pure/simplifier.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Pure/simplifier.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -389,7 +389,7 @@
 
     (*no premature instantiation of variables during simplification*)
     fun safe_solver_tac ctxt =
-      FIRST' [match_tac (trivialities @ Raw_Simplifier.prems_of ctxt), eq_assume_tac];
+      FIRST' [match_tac ctxt (trivialities @ Raw_Simplifier.prems_of ctxt), eq_assume_tac];
     val safe_solver = mk_solver "easy safe" safe_solver_tac;
 
     fun mk_eq thm =
isabelle