--- a/src/HOL/Modelcheck/mucke_oracle.ML Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Tue Sep 06 16:24:53 2005 +0200
@@ -1,8 +1,6 @@
(* $Id$ *)
-exception MuckeOracleExn of term;
-
val trace_mc = ref false;
@@ -1017,9 +1015,8 @@
end;
(**********************************************************)
-(* mk_mc_oracle: new argument of MuckeOracleExn: source_thy *)
-fun mk_mucke_mc_oracle (sign, MuckeOracleExn (subgoal)) =
+fun mk_mc_mucke_oracle sign subgoal =
let val Freesubgoal = freeze_thaw subgoal;
val prems = Logic.strip_imp_prems Freesubgoal;