# HG changeset patch
# User haftmann
# Date 1272483665 -7200
# Node ID 353041483b9b97c4a2ce7dbff2eb3989941aa089
# Parent  8dac276ab10d698c58aaa9342a71f80f85965a0d
use code_reflect

diff -r 8dac276ab10d -r 353041483b9b src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Wed Apr 28 17:04:56 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Apr 28 21:41:05 2010 +0200
@@ -3209,47 +3209,13 @@
   interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_powr interpret_floatarith_log
   interpret_floatarith_sin
 
-ML {*
-structure Float_Arith =
-struct
-
-@{code_datatype float = Float}
-@{code_datatype floatarith = Add | Minus | Mult | Inverse | Cos | Arctan
-                           | Abs | Max | Min | Pi | Sqrt | Exp | Ln | Power | Var | Num }
-@{code_datatype form = Bound | Assign | Less | LessEqual | AtLeastAtMost}
-
-val approx_form = @{code approx_form}
-val approx_tse_form = @{code approx_tse_form}
-val approx' = @{code approx'}
-val approx_form_eval = @{code approx_form_eval}
-
-end
-*}
-
-code_reserved Eval Float_Arith
-
-code_type float (Eval "Float'_Arith.float")
-code_const Float (Eval "Float'_Arith.Float/ (_,/ _)")
-
-code_type floatarith (Eval "Float'_Arith.floatarith")
-code_const Add and Minus and Mult and Inverse and Cos and Arctan and Abs and Max and Min and
-           Pi and Sqrt  and Exp and Ln and Power and Var and Num
-  (Eval "Float'_Arith.Add/ (_,/ _)" and "Float'_Arith.Minus" and "Float'_Arith.Mult/ (_,/ _)" and
-        "Float'_Arith.Inverse" and "Float'_Arith.Cos" and
-        "Float'_Arith.Arctan" and "Float'_Arith.Abs" and "Float'_Arith.Max/ (_,/ _)" and
-        "Float'_Arith.Min/ (_,/ _)" and "Float'_Arith.Pi" and "Float'_Arith.Sqrt" and
-        "Float'_Arith.Exp" and "Float'_Arith.Ln" and "Float'_Arith.Power/ (_,/ _)" and
-        "Float'_Arith.Var" and "Float'_Arith.Num")
-
-code_type form (Eval "Float'_Arith.form")
-code_const Bound and Assign and Less and LessEqual and AtLeastAtMost
-      (Eval "Float'_Arith.Bound/ (_,/ _,/ _,/ _)" and "Float'_Arith.Assign/ (_,/ _,/ _)" and
-            "Float'_Arith.Less/ (_,/ _)" and "Float'_Arith.LessEqual/ (_,/ _)"  and
-            "Float'_Arith.AtLeastAtMost/ (_,/ _,/ _)")
-
-code_const approx_form (Eval "Float'_Arith.approx'_form")
-code_const approx_tse_form (Eval "Float'_Arith.approx'_tse'_form")
-code_const approx' (Eval "Float'_Arith.approx'")
+code_reflect
+  datatypes float = Float
+  and floatarith = Add | Minus | Mult | Inverse | Cos | Arctan
+    | Abs | Max | Min | Pi | Sqrt | Exp | Ln | Power | Var | Num
+  and form = Bound | Assign | Less | LessEqual | AtLeastAtMost
+  functions approx_form approx_tse_form approx' approx_form_eval
+  module_name Float_Arith
 
 ML {*
   fun reorder_bounds_tac prems i =
diff -r 8dac276ab10d -r 353041483b9b 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
diff -r 8dac276ab10d -r 353041483b9b src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Wed Apr 28 17:04:56 2010 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Wed Apr 28 21:41:05 2010 +0200
@@ -5791,8 +5791,10 @@
 ML {* @{code test4} () *}
 ML {* @{code test5} () *}
 
-(*export_code mircfrqe mirlfrqe
-  in SML module_name Mir file "raw_mir.ML"*)
+(*code_reflect
+  functions mircfrqe mirlfrqe
+  module_name Mir
+  file "mir.ML"*)
 
 oracle mirfr_oracle = {* fn (proofs, ct) =>
 let