# HG changeset patch
# User wenzelm
# Date 1248972232 -7200
# Node ID ab9b66c2bbca7f655fc0e40b374346658f939e1a
# Parent  d8ee8a956f19d5060471351281f1b5f1a4b22542
trancl_tac etc.: back to static context -- problem was caused by bad solver in AFP/JiveDataStoreModel;

diff -r d8ee8a956f19 -r ab9b66c2bbca src/Provers/quasi.ML
--- 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);
diff -r d8ee8a956f19 -r ab9b66c2bbca src/Provers/trancl.ML
--- 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;