# HG changeset patch
# User wenzelm
# Date 1125758845 -7200
# Node ID 62bb8dcc316ea0848d9431035c9e5b6075790251
# Parent  f197d8e8d4d25b4c877dcce74915ecb2c8851c5e
simplified oracle;

diff -r f197d8e8d4d2 -r 62bb8dcc316e src/HOLCF/IOA/Modelcheck/MuIOA.ML
--- 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;
 
diff -r f197d8e8d4d2 -r 62bb8dcc316e src/HOLCF/IOA/Modelcheck/MuIOAOracle.ML
--- 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;