changeset 59498 | 50b60f501b05 |
parent 59058 | a78612c67ec0 |
child 59582 | 0fbed69ff081 |
--- a/src/Pure/raw_simplifier.ML Tue Feb 10 14:29:36 2015 +0100 +++ b/src/Pure/raw_simplifier.ML Tue Feb 10 14:48:26 2015 +0100 @@ -1309,7 +1309,7 @@ in bottomc (mode, Option.map (Drule.flexflex_unique (SOME ctxt)) oo prover, maxidx) ctxt ct end; val simple_prover = - SINGLE o (fn ctxt => ALLGOALS (resolve_tac (prems_of ctxt))); + SINGLE o (fn ctxt => ALLGOALS (resolve_tac ctxt (prems_of ctxt))); fun rewrite _ _ [] = Thm.reflexive | rewrite ctxt full thms =