trancl_tac etc.: back to static context -- problem was caused by bad solver in AFP/JiveDataStoreModel;
--- a/src/Provers/quasi.ML Thu Jul 30 17:54:57 2009 +0200
+++ b/src/Provers/quasi.ML Thu Jul 30 18:43:52 2009 +0200
@@ -551,7 +551,7 @@
fun trans_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
let
- val thy = Thm.theory_of_thm st;
+ val thy = ProofContext.theory_of ctxt;
val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
@@ -572,7 +572,7 @@
fun quasi_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
let
- val thy = Thm.theory_of_thm st;
+ val thy = ProofContext.theory_of ctxt
val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
--- 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;