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;