diff -r 245ff8661b8c -r c708ea5b109a src/HOL/Complex/ex/MIR.thy
--- a/src/HOL/Complex/ex/MIR.thy	Mon Aug 20 18:07:31 2007 +0200
+++ b/src/HOL/Complex/ex/MIR.thy	Mon Aug 20 18:07:49 2007 +0200
@@ -5772,10 +5772,10 @@
 definition
   "test5 (u\<Colon>unit) = mircfrqe (A(E(And (Ge(Sub (Bound 1) (Bound 0))) (Eq (Add (Floor (Bound 1)) (Floor (Neg(Bound 0))))))))"
 
-code_gen mircfrqe mirlfrqe test1 test2 test3 test4 test5
+export_code mircfrqe mirlfrqe test1 test2 test3 test4 test5
   in SML module_name Mir
 
-(*code_gen mircfrqe mirlfrqe
+(*export_code mircfrqe mirlfrqe
   in SML module_name Mir file "raw_mir.ML"*)
 
 ML "set Toplevel.timing"