--- a/src/Provers/trancl.ML Wed Jul 29 19:36:22 2009 +0200
+++ b/src/Provers/trancl.ML Wed Jul 29 22:34:31 2009 +0200
@@ -531,9 +531,9 @@
end;
-fun trancl_tac ctxt = SUBGOAL (fn (A, n) =>
+fun trancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Thm.theory_of_thm st;
val Hs = Logic.strip_assums_hyp A;
val C = Logic.strip_assums_concl A;
val (rel, subgoals, prf) = mkconcl_trancl C;
@@ -543,14 +543,14 @@
in
FOCUS (fn {prems, ...} =>
let val thms = map (prove thy rel prems) prfs
- in rtac (prove thy rel thms prf) 1 end) ctxt n
+ in rtac (prove thy rel thms prf) 1 end) ctxt n st
end
- handle Cannot => no_tac);
+ handle Cannot => Seq.empty);
fun rtrancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = Thm.theory_of_thm st;
val Hs = Logic.strip_assums_hyp A;
val C = Logic.strip_assums_concl A;
val (rel, subgoals, prf) = mkconcl_rtrancl C;