--- 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),
--- 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)
--- 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,