src/HOL/Decision_Procs/commutative_ring_tac.ML
changeset 42361 23f352990944
parent 38864 4abe644fcea5
child 44121 44adaa6db327
     1.1 --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Sat Apr 16 15:47:52 2011 +0200
     1.2 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Sat Apr 16 16:15:37 2011 +0200
     1.3 @@ -86,7 +86,7 @@
     1.4  
     1.5  fun tac ctxt = SUBGOAL (fn (g, i) =>
     1.6    let
     1.7 -    val thy = ProofContext.theory_of ctxt;
     1.8 +    val thy = Proof_Context.theory_of ctxt;
     1.9      val cring_ss = Simplifier.simpset_of ctxt  (*FIXME really the full simpset!?*)
    1.10        addsimps cring_simps;
    1.11      val (ca, cvs, clhs, crhs) = reif_eq thy (HOLogic.dest_Trueprop g)