author wenzelm Wed, 29 Jul 2009 22:34:31 +0200 changeset 32277 ff1e59a15146 parent 32275 b10cbf4d3f55 child 32278 f73d48f5218b
trans_tac: use theory from goal state, not the static context, which seems to be outdated under certain circumstances (why?);
 src/Provers/quasi.ML file | annotate | diff | comparison | revisions src/Provers/trancl.ML file | annotate | diff | comparison | revisions
```--- a/src/Provers/quasi.ML	Wed Jul 29 19:36:22 2009 +0200
+++ b/src/Provers/quasi.ML	Wed Jul 29 22:34:31 2009 +0200
@@ -549,9 +549,9 @@

(* trans_tac - solves transitivity chains over <= *)

-fun trans_tac ctxt = SUBGOAL (fn (A, n) =>
+fun trans_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
let
-  val thy = ProofContext.theory_of ctxt;
+  val thy = Thm.theory_of_thm st;
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);
@@ -562,17 +562,17 @@
in
FOCUS (fn {prems, ...} =>
let val thms = map (prove prems) prfs
-    in rtac (prove thms prf) 1 end) ctxt n
+    in rtac (prove thms prf) 1 end) ctxt n st
end
- handle Contr p => FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n
-  | Cannot  => no_tac);
+ handle Contr p => FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
+  | Cannot  => Seq.empty);

(* quasi_tac - solves quasi orders *)

fun quasi_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
let
-  val thy = ProofContext.theory_of ctxt;
+  val thy = Thm.theory_of_thm st;
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	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;```