src/Provers/trancl.ML

 end;
 
 
 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;
 
   val prems = flat (map_index (mkasm_trancl rel o swap) Hs);

  handle Cannot => Seq.empty);
 
 
 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;
 
   val prems = flat (map_index (mkasm_rtrancl rel o swap) Hs);