src/Provers/trancl.ML
changeset 32285 ab9b66c2bbca
parent 32283 3bebc195c124
child 32740 9dd0a2f83429
--- a/src/Provers/trancl.ML	Thu Jul 30 17:54:57 2009 +0200
+++ b/src/Provers/trancl.ML	Thu Jul 30 18:43:52 2009 +0200
@@ -533,7 +533,7 @@
 
 fun trancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
  let
-  val thy = Thm.theory_of_thm st;
+  val thy = ProofContext.theory_of ctxt;
   val Hs = Logic.strip_assums_hyp A;
   val C = Logic.strip_assums_concl A;
   val (rel, subgoals, prf) = mkconcl_trancl C;
@@ -550,7 +550,7 @@
 
 fun rtrancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
  let
-  val thy = Thm.theory_of_thm st;
+  val thy = ProofContext.theory_of ctxt;
   val Hs = Logic.strip_assums_hyp A;
   val C = Logic.strip_assums_concl A;
   val (rel, subgoals, prf) = mkconcl_rtrancl C;