--- a/src/Provers/trancl.ML Tue Feb 10 14:29:36 2015 +0100
+++ b/src/Provers/trancl.ML Tue Feb 10 14:48:26 2015 +0100
@@ -541,11 +541,11 @@
val prems = flat (map_index (mkasm_trancl rel o swap) Hs);
val prfs = solveTrancl (prems, C);
in
- Subgoal.FOCUS (fn {prems, concl, ...} =>
+ Subgoal.FOCUS (fn {context = ctxt', prems, concl, ...} =>
let
val SOME (_, _, rel', _) = decomp (term_of concl);
val thms = map (prove thy rel' prems) prfs
- in resolve_tac [prove thy rel' thms prf] 1 end) ctxt n st
+ in resolve_tac ctxt' [prove thy rel' thms prf] 1 end) ctxt n st
end
handle Cannot => Seq.empty);
@@ -560,11 +560,11 @@
val prems = flat (map_index (mkasm_rtrancl rel o swap) Hs);
val prfs = solveRtrancl (prems, C);
in
- Subgoal.FOCUS (fn {prems, concl, ...} =>
+ Subgoal.FOCUS (fn {context = ctxt', prems, concl, ...} =>
let
val SOME (_, _, rel', _) = decomp (term_of concl);
val thms = map (prove thy rel' prems) prfs
- in resolve_tac [prove thy rel' thms prf] 1 end) ctxt n st
+ in resolve_tac ctxt' [prove thy rel' thms prf] 1 end) ctxt n st
end
handle Cannot => Seq.empty | General.Subscript => Seq.empty);