changeset 42361 | 23f352990944 |
parent 41539 | 0e02dd4f87f0 |
child 44945 | 2625de88c994 |
--- a/src/HOL/Tools/arith_data.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/arith_data.ML Sat Apr 16 16:15:37 2011 +0200 @@ -53,7 +53,7 @@ fun gen_arith_tac verbose ctxt = let - val tactics = Arith_Tactics.get (ProofContext.theory_of ctxt); + val tactics = Arith_Tactics.get (Proof_Context.theory_of ctxt); fun invoke (_, (name, tac)) k st = tac verbose ctxt k st; in FIRST' (map invoke (rev tactics)) end;