1.1 --- a/src/Provers/quasi.ML	Wed Jul 29 21:40:04 2009 +0200
     1.2 +++ b/src/Provers/quasi.ML	Wed Jul 29 22:38:35 2009 +0200
     1.3 @@ -549,9 +549,9 @@
     1.4  
     1.5  (* trans_tac - solves transitivity chains over <= *)
     1.6  
     1.7 -fun trans_tac ctxt = SUBGOAL (fn (A, n) =>
     1.8 +fun trans_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
     1.9   let
    1.10 -  val thy = ProofContext.theory_of ctxt;
    1.11 +  val thy = Thm.theory_of_thm st;
    1.12    val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
    1.13    val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
    1.14    val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
    1.15 @@ -562,17 +562,17 @@
    1.16   in
    1.17    FOCUS (fn {prems, ...} =>
    1.18      let val thms = map (prove prems) prfs
    1.19 -    in rtac (prove thms prf) 1 end) ctxt n
    1.20 +    in rtac (prove thms prf) 1 end) ctxt n st
    1.21   end
    1.22 - handle Contr p => FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n
    1.23 -  | Cannot  => no_tac);
    1.24 + handle Contr p => FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
    1.25 +  | Cannot  => Seq.empty);
    1.26  
    1.27  
    1.28  (* quasi_tac - solves quasi orders *)
    1.29  
    1.30  fun quasi_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
    1.31   let
    1.32 -  val thy = ProofContext.theory_of ctxt;
    1.33 +  val thy = Thm.theory_of_thm st;
    1.34    val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
    1.35    val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
    1.36    val C = subst_bounds (rfrees, Logic.strip_assums_concl A);

     2.1 --- a/src/Provers/trancl.ML	Wed Jul 29 21:40:04 2009 +0200
     2.2 +++ b/src/Provers/trancl.ML	Wed Jul 29 22:38:35 2009 +0200
     2.3 @@ -531,9 +531,9 @@
     2.4  end;
     2.5  
     2.6  
     2.7 -fun trancl_tac ctxt = SUBGOAL (fn (A, n) =>
     2.8 +fun trancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
     2.9   let
    2.10 -  val thy = ProofContext.theory_of ctxt;
    2.11 +  val thy = Thm.theory_of_thm st;
    2.12    val Hs = Logic.strip_assums_hyp A;
    2.13    val C = Logic.strip_assums_concl A;
    2.14    val (rel, subgoals, prf) = mkconcl_trancl C;
    2.15 @@ -543,14 +543,14 @@
    2.16   in
    2.17    FOCUS (fn {prems, ...} =>
    2.18      let val thms = map (prove thy rel prems) prfs
    2.19 -    in rtac (prove thy rel thms prf) 1 end) ctxt n
    2.20 +    in rtac (prove thy rel thms prf) 1 end) ctxt n st
    2.21   end
    2.22 - handle Cannot => no_tac);
    2.23 + handle Cannot => Seq.empty);
    2.24  
    2.25  
    2.26  fun rtrancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
    2.27   let
    2.28 -  val thy = ProofContext.theory_of ctxt;
    2.29 +  val thy = Thm.theory_of_thm st;
    2.30    val Hs = Logic.strip_assums_hyp A;
    2.31    val C = Logic.strip_assums_concl A;
    2.32    val (rel, subgoals, prf) = mkconcl_rtrancl C;