# HG changeset patch
# User wenzelm
# Date 1117533223 -7200
# Node ID 7294283b0c453833e845fc0803e9ea27ed6b372f
# Parent  cf7f146086bc539a90678b4c7c58e682fccc7319
no_tac;

diff -r cf7f146086bc -r 7294283b0c45 src/HOL/Modelcheck/MuckeSyn.ML
--- a/src/HOL/Modelcheck/MuckeSyn.ML	Tue May 31 11:53:42 2005 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.ML	Tue May 31 11:53:43 2005 +0200
@@ -1,3 +1,6 @@
+
+(* $Id$ *)
+
 (* search_mu t searches for Mu terms in term t. In the case of nested Mu's,
    it yields innermost one. If no Mu term is present, search_mu yields NONE
 *)
@@ -167,7 +170,7 @@
 
 fun mc_mucke_tac defs i state =
   (case Library.drop (i - 1, Thm.prems_of state) of
-    [] => PureGeneral.Seq.empty
+    [] => no_tac state
   | subgoal :: _ =>
       EVERY [
         REPEAT (etac thin_rl i),
diff -r cf7f146086bc -r 7294283b0c45 src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Tue May 31 11:53:42 2005 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Tue May 31 11:53:43 2005 +0200
@@ -1,3 +1,6 @@
+
+(* $Id$ *)
+
 exception MuckeOracleExn of term;
 
 val trace_mc = ref false; 
@@ -102,7 +105,7 @@
 	val prems = prems @ [concl];
         val itrm = search_ifs prems;
 in
-if (itrm = []) then (PureGeneral.Seq.empty) else
+if (itrm = []) then no_tac state else
 (
 let
 val trm = hd(itrm)
diff -r cf7f146086bc -r 7294283b0c45 src/HOLCF/IOA/Modelcheck/MuIOAOracle.ML
--- a/src/HOLCF/IOA/Modelcheck/MuIOAOracle.ML	Tue May 31 11:53:42 2005 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOAOracle.ML	Tue May 31 11:53:43 2005 +0200
@@ -1,3 +1,5 @@
+
+(* $Id$ *)
 
 (* call_sim_tac invokes oracle "Sim" *)
 fun call_sim_tac thm_list i state = 
@@ -14,7 +16,7 @@
 let val sign = #sign (rep_thm state);
 in
 case Library.drop(i-1,prems_of state) of
-        [] => PureGeneral.Seq.empty |
+        [] => no_tac state |
         subgoal::_ => EVERY[REPEAT(etac thin_rl i),
                         simp_tac (simpset() addsimps [ioa_implements_def]) i,
                         rtac conjI i,