--- a/src/HOL/Modelcheck/MCSyn.ML Thu Oct 09 14:59:36 1997 +0200
+++ b/src/HOL/Modelcheck/MCSyn.ML Thu Oct 09 15:00:41 1997 +0200
@@ -11,7 +11,7 @@
[] => Sequence.null |
subgoal::_ =>
let val concl = Logic.strip_imp_concl subgoal;
- val OraAss = invoke_oracle(MCSyn.thy,sign,MCOracleExn concl);
+ val OraAss = invoke_oracle MCSyn.thy "mc" (sign,MCOracleExn concl);
in
((cut_facts_tac [OraAss] i) THEN (atac i)) state
end
--- a/src/HOL/Modelcheck/MCSyn.thy Thu Oct 09 14:59:36 1997 +0200
+++ b/src/HOL/Modelcheck/MCSyn.thy Thu Oct 09 15:00:41 1997 +0200
@@ -28,6 +28,6 @@
"Nu " :: [idts, 'a pred] => 'a pred ("(3[nu _./ _])" 1000)
oracle
- mk_mc_oracle
+ mc = mk_mc_oracle
end
--- a/src/HOL/Modelcheck/MuCalculus.ML Thu Oct 09 14:59:36 1997 +0200
+++ b/src/HOL/Modelcheck/MuCalculus.ML Thu Oct 09 15:00:41 1997 +0200
@@ -10,6 +10,7 @@
val trace_mc = ref false;
+local
fun termtext sign term =
setmp print_mode ["Eindhoven"]
@@ -18,6 +19,7 @@
fun call_mc s =
execute ( "echo \"" ^ s ^ "\" | pmu -w" );
+in
fun mk_mc_oracle (sign, MCOracleExn trm) =
let
@@ -33,3 +35,5 @@
"FALSE\n" => (error "MC oracle yields FALSE") |
_ => (error ("MC syntax error: " ^ result)))
end;
+
+end;