--- a/src/HOL/ex/Reflected_Presburger.thy Mon Aug 20 18:07:31 2007 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy Mon Aug 20 18:07:49 2007 +0200
@@ -1937,8 +1937,8 @@
(Bound 2))))))))"
code_reserved SML oo
-code_gen pa cooper_test in SML module_name GeneratedCooper
-(*code_gen pa in SML module_name GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"*)
+export_code pa cooper_test in SML module_name GeneratedCooper
+(*export_code pa in SML module_name GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"*)
ML {* GeneratedCooper.cooper_test () *}
use "coopereif.ML"