src/HOL/ex/Reflected_Presburger.thy

   "cooper_test u = pa (E (A (Imp (Ge (Sub (Bound 0) (Bound 1)))
     (E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0)))
       (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"
 oracle linzqe_oracle ("term") = Coopereif.cooper_oracle
 use "coopertac.ML"