src/HOL/Decision_Procs/MIR.thy

--- a/src/HOL/Decision_Procs/MIR.thy	Wed Apr 28 17:04:56 2010 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Wed Apr 28 21:41:05 2010 +0200
@@ -5791,8 +5791,10 @@
 ML {* @{code test4} () *}
 ML {* @{code test5} () *}
 
-(*export_code mircfrqe mirlfrqe
-  in SML module_name Mir file "raw_mir.ML"*)
+(*code_reflect
+  functions mircfrqe mirlfrqe
+  module_name Mir
+  file "mir.ML"*)
 
 oracle mirfr_oracle = {* fn (proofs, ct) =>
 let