changeset 50107 | 289181e3e524 |
parent 47967 | c422128d3889 |
child 50111 | 9e04e6edc5e7 |
--- a/src/Provers/clasimp.ML Sat Nov 17 17:42:19 2012 +0100 +++ b/src/Provers/clasimp.ML Sat Nov 17 17:55:52 2012 +0100 @@ -44,9 +44,6 @@ (* simp as classical wrapper *) -(*not totally safe: may instantiate unknowns that appear also in other subgoals*) -val safe_asm_full_simp_tac = Simplifier.generic_simp_tac true (true, true, true); - fun clasimp f name tac ctxt = Classical.map_claset (fn cs => f (cs, (name, CHANGED o tac (simpset_of ctxt)))) ctxt;