src/HOL/Decision_Procs/Cooper.thy

   where
     "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))))))))"
 
-ML {* @{code cooper_test} () *}
+ML_val {* @{code cooper_test} () *}
 
 (*code_reflect Cooper_Procedure
   functions pa
   file "~~/src/HOL/Tools/Qelim/cooper_procedure.ML"*)