--- a/src/HOLCF/IOA/Modelcheck/MuIOA.ML Sat Sep 03 16:46:56 2005 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.ML Sat Sep 03 16:47:25 2005 +0200
@@ -3,7 +3,6 @@
There, implementation relations for I/O automatons are proved using
the model checker mucke (invoking cal_mucke_tac defined in MCSyn.ML). *)
-exception SimOracleExn of (term*(thm list));
exception SimFailureExn of string;
val ioa_simps = [asig_of_def,starts_of_def,trans_of_def];
@@ -162,7 +161,7 @@
in
-fun mk_sim_oracle (sign, SimOracleExn (subgoal,thl)) =
+fun mk_sim_oracle sign (subgoal,thl) =
(let
val weak_case_congs = DatatypePackage.weak_case_congs_of sign;
--- a/src/HOLCF/IOA/Modelcheck/MuIOAOracle.ML Sat Sep 03 16:46:56 2005 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOAOracle.ML Sat Sep 03 16:47:25 2005 +0200
@@ -5,7 +5,7 @@
fun call_sim_tac thm_list i state =
let val sign = #sign (rep_thm state);
val (subgoal::_) = Library.drop(i-1,prems_of state);
- val OraAss = invoke_oracle MuIOAOracle.thy "Sim" (sign,SimOracleExn (subgoal,thm_list));
+ val OraAss = sim_oracle sign (subgoal,thm_list);
in
(cut_facts_tac [OraAss] i) state
end;