changeset 17241 | 62bb8dcc316e |
parent 16152 | 7294283b0c45 |
child 19741 | f65265d71426 |
--- 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;