src/HOL/Decision_Procs/Cooper.thy

--- a/src/HOL/Decision_Procs/Cooper.thy	Wed Apr 28 17:04:56 2010 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Wed Apr 28 21:41:05 2010 +0200
@@ -1909,10 +1909,10 @@
 
 ML {* @{code cooper_test} () *}
 
-(*
-code_reserved SML oo
-export_code pa in SML module_name GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"
-*)
+code_reflect
+  functions pa
+  module_name Generated_Cooper
+  file "~~/src/HOL/Tools/Qelim/generated_cooper.ML"
 
 oracle linzqe_oracle = {*
 let