# HG changeset patch
# User haftmann
# Date 1272546040 -7200
# Node ID 19f6e3b0d9b6f1a9b5686c89f3ba48beae30f998
# Parent  01dd308897882e6ebafd04f33cd3a4d0254cc1fe
code_reflect: specify module name directly after keyword

diff -r 01dd30889788 -r 19f6e3b0d9b6 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Thu Apr 29 15:00:39 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Apr 29 15:00:40 2010 +0200
@@ -3209,13 +3209,12 @@
   interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_powr interpret_floatarith_log
   interpret_floatarith_sin
 
-code_reflect
+code_reflect Float_Arith
   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 01dd30889788 -r 19f6e3b0d9b6 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Thu Apr 29 15:00:39 2010 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Thu Apr 29 15:00:40 2010 +0200
@@ -1909,9 +1909,8 @@
 
 ML {* @{code cooper_test} () *}
 
-code_reflect
+code_reflect Generated_Cooper
   functions pa
-  module_name Generated_Cooper
   file "~~/src/HOL/Tools/Qelim/generated_cooper.ML"
 
 oracle linzqe_oracle = {*
diff -r 01dd30889788 -r 19f6e3b0d9b6 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Thu Apr 29 15:00:39 2010 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Thu Apr 29 15:00:40 2010 +0200
@@ -5791,9 +5791,8 @@
 ML {* @{code test4} () *}
 ML {* @{code test5} () *}
 
-(*code_reflect
+(*code_reflect Mir
   functions mircfrqe mirlfrqe
-  module_name Mir
   file "mir.ML"*)
 
 oracle mirfr_oracle = {* fn (proofs, ct) =>
diff -r 01dd30889788 -r 19f6e3b0d9b6 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Thu Apr 29 15:00:39 2010 +0200
+++ b/src/HOL/Predicate.thy	Thu Apr 29 15:00:40 2010 +0200
@@ -880,10 +880,9 @@
 
 code_abort not_unique
 
-code_reflect
+code_reflect Predicate
   datatypes pred = Seq and seq = Empty | Insert | Join
   functions map
-  module_name Predicate
 
 ML {*
 signature PREDICATE =