# HG changeset patch
# User wenzelm
# Date 876402041 -7200
# Node ID 5a1116b69196d2cfa0dbcd1110cad2934225f442
# Parent  f20f193d42b4472f6971c123285461b4bc90d016
fixed oracle;

diff -r f20f193d42b4 -r 5a1116b69196 src/HOL/Modelcheck/MCSyn.ML
--- 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
diff -r f20f193d42b4 -r 5a1116b69196 src/HOL/Modelcheck/MCSyn.thy
--- 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
diff -r f20f193d42b4 -r 5a1116b69196 src/HOL/Modelcheck/MuCalculus.ML
--- 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;