src/Provers/trancl.ML
changeset 42361 23f352990944
parent 37744 3daaf23b9ab4
child 42364 8c674b3b8e44
--- a/src/Provers/trancl.ML	Sat Apr 16 15:47:52 2011 +0200
+++ b/src/Provers/trancl.ML	Sat Apr 16 16:15:37 2011 +0200
@@ -534,7 +534,7 @@
 
 fun trancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
  let
-  val thy = ProofContext.theory_of ctxt;
+  val thy = Proof_Context.theory_of ctxt;
   val Hs = Logic.strip_assums_hyp A;
   val C = Logic.strip_assums_concl A;
   val (rel, subgoals, prf) = mkconcl_trancl C;
@@ -553,7 +553,7 @@
 
 fun rtrancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
  let
-  val thy = ProofContext.theory_of ctxt;
+  val thy = Proof_Context.theory_of ctxt;
   val Hs = Logic.strip_assums_hyp A;
   val C = Logic.strip_assums_concl A;
   val (rel, subgoals, prf) = mkconcl_rtrancl C;