# HG changeset patch
# User haftmann
# Date 1187032957 -7200
# Node ID 1f60b45c5f973adbc13b0397239a8fe6e2f232e7
# Parent  d276e4b53d6bee6a8920ab43249ae5c09fabea53
renamed keyword "to" to "module_name"

diff -r d276e4b53d6b -r 1f60b45c5f97 etc/isar-keywords-HOL-Nominal.el
--- a/etc/isar-keywords-HOL-Nominal.el	Mon Aug 13 21:22:36 2007 +0200
+++ b/etc/isar-keywords-HOL-Nominal.el	Mon Aug 13 21:22:37 2007 +0200
@@ -221,7 +221,6 @@
     "undo"
     "undos_proof"
     "unfolding"
-    "update_thy"
     "use"
     "use_thy"
     "using"
@@ -262,6 +261,7 @@
     "inject"
     "invariant"
     "is"
+    "module_name"
     "monos"
     "morphisms"
     "notes"
@@ -274,7 +274,6 @@
     "sequential"
     "shows"
     "structure"
-    "to"
     "unchecked"
     "uses"
     "where"))
@@ -356,7 +355,6 @@
     "touch_child_thys"
     "touch_thy"
     "typ"
-    "update_thy"
     "use"
     "use_thy"
     "value"
diff -r d276e4b53d6b -r 1f60b45c5f97 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Mon Aug 13 21:22:36 2007 +0200
+++ b/etc/isar-keywords-ZF.el	Mon Aug 13 21:22:37 2007 +0200
@@ -110,7 +110,6 @@
     "no_syntax"
     "no_translations"
     "nonterminals"
-    "normal_form"
     "notation"
     "note"
     "obtain"
@@ -202,7 +201,6 @@
     "undo"
     "undos_proof"
     "unfolding"
-    "update_thy"
     "use"
     "use_thy"
     "using"
@@ -241,6 +239,7 @@
     "infixr"
     "intros"
     "is"
+    "module_name"
     "monos"
     "notes"
     "obtains"
@@ -250,7 +249,6 @@
     "recursor_eqns"
     "shows"
     "structure"
-    "to"
     "type_elims"
     "type_intros"
     "unchecked"
@@ -290,7 +288,6 @@
     "header"
     "help"
     "kill_thy"
-    "normal_form"
     "pr"
     "pretty_setmargin"
     "prf"
@@ -332,7 +329,6 @@
     "touch_child_thys"
     "touch_thy"
     "typ"
-    "update_thy"
     "use"
     "use_thy"
     "value"
diff -r d276e4b53d6b -r 1f60b45c5f97 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Mon Aug 13 21:22:36 2007 +0200
+++ b/etc/isar-keywords.el	Mon Aug 13 21:22:37 2007 +0200
@@ -222,7 +222,6 @@
     "undo"
     "undos_proof"
     "unfolding"
-    "update_thy"
     "use"
     "use_thy"
     "using"
@@ -267,6 +266,7 @@
     "internals"
     "is"
     "lazy"
+    "module_name"
     "monos"
     "morphisms"
     "notes"
@@ -370,7 +370,6 @@
     "touch_child_thys"
     "touch_thy"
     "typ"
-    "update_thy"
     "use"
     "use_thy"
     "value"
diff -r d276e4b53d6b -r 1f60b45c5f97 src/HOL/Complex/ex/MIR.thy
--- a/src/HOL/Complex/ex/MIR.thy	Mon Aug 13 21:22:36 2007 +0200
+++ b/src/HOL/Complex/ex/MIR.thy	Mon Aug 13 21:22:37 2007 +0200
@@ -5778,9 +5778,10 @@
   "test5 (u\<Colon>unit) = mircfrqe (A(E(And (Ge(Sub (Bound 1) (Bound 0))) (Eq (Add (Floor (Bound 1)) (Floor (Neg(Bound 0))))))))"
 
 code_gen mircfrqe mirlfrqe test1 test2 test3 test4 test5
-  in SML to Mir
-
-code_gen mircfrqe mirlfrqe in SML to Mir file "raw_mir.ML"
+  in SML module_name Mir
+
+(*code_gen mircfrqe mirlfrqe
+  in SML module_name Mir file "raw_mir.ML"*)
 
 ML "set Toplevel.timing"
 ML "Mir.test1 ()"
diff -r d276e4b53d6b -r 1f60b45c5f97 src/HOL/Complex/ex/ReflectedFerrack.thy
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Mon Aug 13 21:22:36 2007 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Mon Aug 13 21:22:37 2007 +0200
@@ -1993,7 +1993,7 @@
   "ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0)))
     (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))"
 
-code_gen linrqe ferrack_test in SML to Ferrack
+code_gen linrqe ferrack_test in SML module_name Ferrack
 
 (*code_module Ferrack
   contains
diff -r d276e4b53d6b -r 1f60b45c5f97 src/HOL/Extraction/Higman.thy
--- a/src/HOL/Extraction/Higman.thy	Mon Aug 13 21:22:36 2007 +0200
+++ b/src/HOL/Extraction/Higman.thy	Mon Aug 13 21:22:37 2007 +0200
@@ -427,7 +427,7 @@
 code_datatype L0 L1 arbitrary_LT
 code_datatype T0 T1 T2 arbitrary_TT
 
-code_gen higman_idx in SML to Higman
+code_gen higman_idx in SML module_name Higman
 
 ML {*
 local
diff -r d276e4b53d6b -r 1f60b45c5f97 src/HOL/Extraction/Pigeonhole.thy
--- a/src/HOL/Extraction/Pigeonhole.thy	Mon Aug 13 21:22:36 2007 +0200
+++ b/src/HOL/Extraction/Pigeonhole.thy	Mon Aug 13 21:22:37 2007 +0200
@@ -303,36 +303,36 @@
   (* this is justified since for valid inputs this "arbitrary" will be dropped
      in the next recursion step in pigeonhole_def *)
 
-code_module PH
+code_module PH1
 contains
   test = test
   test' = test'
   test'' = test''
 
-code_gen test test' test'' in SML to PH2
+code_gen test test' test'' in SML module_name PH2
 
-ML "timeit (PH.test 10)"
+ML "timeit (PH1.test 10)"
 ML "timeit (PH2.test 10)"
 
-ML "timeit (PH.test' 10)"
+ML "timeit (PH1.test' 10)"
 ML "timeit (PH2.test' 10)"
 
-ML "timeit (PH.test 20)"
+ML "timeit (PH1.test 20)"
 ML "timeit (PH2.test 20)"
 
-ML "timeit (PH.test' 20)"
+ML "timeit (PH1.test' 20)"
 ML "timeit (PH2.test' 20)"
 
-ML "timeit (PH.test 25)"
+ML "timeit (PH1.test 25)"
 ML "timeit (PH2.test 25)"
 
-ML "timeit (PH.test' 25)"
+ML "timeit (PH1.test' 25)"
 ML "timeit (PH2.test' 25)"
 
-ML "timeit (PH.test 500)"
+ML "timeit (PH1.test 500)"
 ML "timeit (PH2.test 500)"
 
-ML "timeit PH.test''"
+ML "timeit PH1.test''"
 ML "timeit PH2.test''"
 
 end
diff -r d276e4b53d6b -r 1f60b45c5f97 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Mon Aug 13 21:22:36 2007 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Mon Aug 13 21:22:37 2007 +0200
@@ -581,7 +581,7 @@
   int :: "nat \<Rightarrow> int" where
   "int \<equiv> of_nat"
 
-code_gen type_NF nat int in SML to Norm
+code_gen type_NF nat int in SML module_name Norm
 
 ML {*
 val nat_of_int = Norm.nat o IntInf.fromInt;
diff -r d276e4b53d6b -r 1f60b45c5f97 src/HOL/ex/Classpackage.thy
--- a/src/HOL/ex/Classpackage.thy	Mon Aug 13 21:22:36 2007 +0200
+++ b/src/HOL/ex/Classpackage.thy	Mon Aug 13 21:22:37 2007 +0200
@@ -328,7 +328,7 @@
 definition "x2 = X (1::int) 2 3"
 definition "y2 = Y (1::int) 2 3"
 
-code_gen x1 x2 y2 in SML to Classpackage
+code_gen x1 x2 y2 in SML module_name Classpackage
   in OCaml file -
   in Haskell file -
 
diff -r d276e4b53d6b -r 1f60b45c5f97 src/HOL/ex/Codegenerator.thy
--- a/src/HOL/ex/Codegenerator.thy	Mon Aug 13 21:22:36 2007 +0200
+++ b/src/HOL/ex/Codegenerator.thy	Mon Aug 13 21:22:37 2007 +0200
@@ -8,7 +8,7 @@
 imports ExecutableContent
 begin
 
-code_gen "*" in SML to CodegenTest
+code_gen "*" in SML module_name CodegenTest
   in OCaml file -
   in Haskell file -
 
diff -r d276e4b53d6b -r 1f60b45c5f97 src/HOL/ex/Codegenerator_Pretty.thy
--- a/src/HOL/ex/Codegenerator_Pretty.thy	Mon Aug 13 21:22:36 2007 +0200
+++ b/src/HOL/ex/Codegenerator_Pretty.thy	Mon Aug 13 21:22:37 2007 +0200
@@ -49,7 +49,7 @@
 definition
   "foobar' = (foo' R1' 1 R3', bar' R2' 0 R3', foo' R1' R3' R2')"
 
-code_gen foobar foobar' in SML to Foo
+code_gen foobar foobar' in SML module_name Foo
   in OCaml file -
   in Haskell file -
 ML {* (Foo.foobar, Foo.foobar') *}
diff -r d276e4b53d6b -r 1f60b45c5f97 src/HOL/ex/Reflected_Presburger.thy
--- a/src/HOL/ex/Reflected_Presburger.thy	Mon Aug 13 21:22:36 2007 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy	Mon Aug 13 21:22:37 2007 +0200
@@ -1936,8 +1936,8 @@
       (Bound 2))))))))"
 
 code_reserved SML oo
-code_gen pa cooper_test in SML to GeneratedCooper
-(*code_gen pa in SML to GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"*)
+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"*)
 
 ML {* GeneratedCooper.cooper_test () *}
 use "coopereif.ML"