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)