# HG changeset patch
# User haftmann
# Date 1155555966 -7200
# Node ID 14f9f2a1caa666a64a9a876d4dcb4e0bf3ce7aaf
# Parent  154d8c155a655977fef065ff82ed22690c7cd778
simplified code generator setup

diff -r 154d8c155a65 -r 14f9f2a1caa6 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Mon Aug 14 13:46:05 2006 +0200
+++ b/src/HOL/Divides.thy	Mon Aug 14 13:46:06 2006 +0200
@@ -869,13 +869,6 @@
 apply (rule mod_add1_eq [symmetric])
 done
 
-subsection {* Code generator setup *}
-
-code_alias
-  "Divides.op div" "Divides.div"
-  "Divides.op dvd" "Divides.dvd"
-  "Divides.op mod" "Divides.mod"
-
 ML
 {*
 val div_def = thm "div_def"
diff -r 154d8c155a65 -r 14f9f2a1caa6 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Aug 14 13:46:05 2006 +0200
+++ b/src/HOL/HOL.thy	Mon Aug 14 13:46:06 2006 +0200
@@ -1420,17 +1420,6 @@
   CodegenTheorems.init_obj ((TrueI, FalseE), (conjI, thm "HOL.atomize_eq" |> Thm.symmetric))
 *}
 
-code_alias
-  bool "HOL.bool"
-  True "HOL.True"
-  False "HOL.False"
-  "op =" "HOL.op_eq"
-  "op -->" "HOL.op_implies"
-  "op &" "HOL.op_and"
-  "op |" "HOL.op_or"
-  Not "HOL.not"
-  arbitrary "HOL.arbitrary"
-
 code_constapp
   "op =" (* an intermediate solution for polymorphic equality *)
     ml (infixl 6 "=")
diff -r 154d8c155a65 -r 14f9f2a1caa6 src/HOL/Integ/IntArith.thy
--- a/src/HOL/Integ/IntArith.thy	Mon Aug 14 13:46:05 2006 +0200
+++ b/src/HOL/Integ/IntArith.thy	Mon Aug 14 13:46:06 2006 +0200
@@ -364,16 +364,19 @@
 
 subsection {* code generator setup *}
 
-code_alias
+code_typename
   "Numeral.bin" "IntDef.bin"
   "Numeral.bit" "IntDef.bit"
-  "Numeral.Pls" "IntDef.Pls"
-  "Numeral.Min" "IntDef.Min"
-  "Numeral.Bit" "IntDef.Bit"
-  "Numeral.Abs_Bin" "IntDef.Bin"
+
+code_constname
+  "Numeral.Abs_Bin" "IntDef.bin"
   "Numeral.Rep_Bin" "IntDef.int_of_bin"
-  "Numeral.B0" "IntDef.B0"
-  "Numeral.B1" "IntDef.B1"
+  "Numeral.Pls" "IntDef.pls"
+  "Numeral.Min" "IntDef.min"
+  "Numeral.Bit" "IntDef.bit"
+  "Numeral.bit.bit_case" "IntDef.bit_case"
+  "Numeral.B0" "IntDef.b0"
+  "Numeral.B1" "IntDef.b1"
 
 lemma
   number_of_is_rep_bin [code inline]: "number_of = Rep_Bin"
diff -r 154d8c155a65 -r 14f9f2a1caa6 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Mon Aug 14 13:46:05 2006 +0200
+++ b/src/HOL/Library/ExecutableSet.thy	Mon Aug 14 13:46:06 2006 +0200
@@ -256,7 +256,7 @@
   "Ball"    ("{*Blall*}")
   "Bex"     ("{*Blex*}")
 
-code_alias
+code_constname
   "ExecutableSet.member" "List.member"
   "ExecutableSet.insertl" "List.insertl"
   "ExecutableSet.drop_first" "List.drop_first"
diff -r 154d8c155a65 -r 14f9f2a1caa6 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Aug 14 13:46:05 2006 +0200
+++ b/src/HOL/List.thy	Mon Aug 14 13:46:06 2006 +0200
@@ -2761,10 +2761,6 @@
 
 consts_code "Cons" ("(_ ::/ _)")
 
-code_alias
-  "List.op @" "List.append"
-  "List.op mem" "List.mem"
-
 code_typapp
   list
     ml ("_ list")
@@ -2785,6 +2781,4 @@
 
 setup list_codegen_setup
 
-setup CodegenPackage.rename_inconsistent
-
 end
diff -r 154d8c155a65 -r 14f9f2a1caa6 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Aug 14 13:46:05 2006 +0200
+++ b/src/HOL/Nat.thy	Mon Aug 14 13:46:06 2006 +0200
@@ -1047,10 +1047,4 @@
   "1 = Suc 0"
   by simp
 
-code_alias
-  "nat" "Nat.nat"
-  "0" "Nat.Zero"
-  "1" "Nat.One"
-  "Suc" "Nat.Suc"
-
 end
diff -r 154d8c155a65 -r 14f9f2a1caa6 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon Aug 14 13:46:05 2006 +0200
+++ b/src/HOL/Product_Type.thy	Mon Aug 14 13:46:06 2006 +0200
@@ -772,12 +772,6 @@
 consts_code
   "Pair"    ("(_,/ _)")
 
-code_alias
-  "*" "Product_Type.pair"
-  "Pair" "Product_Type.Pair"
-  "fst" "Product_Type.fst"
-  "snd" "Product_Type.snd"
-
 ML {*
 
 fun strip_abs_split 0 t = ([], t)
diff -r 154d8c155a65 -r 14f9f2a1caa6 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Aug 14 13:46:05 2006 +0200
+++ b/src/HOL/Set.thy	Mon Aug 14 13:46:06 2006 +0200
@@ -2258,10 +2258,4 @@
   ord_eq_less_trans
   trans
 
-subsection {* Code generator setup *}
-
-code_alias
-  "op Int" "Set.inter"
-  "op Un" "Set.union"
-
 end
diff -r 154d8c155a65 -r 14f9f2a1caa6 src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Mon Aug 14 13:46:05 2006 +0200
+++ b/src/HOL/Sum_Type.thy	Mon Aug 14 13:46:06 2006 +0200
@@ -227,11 +227,4 @@
 val basic_monos = thms "basic_monos";
 *}
 
-subsection {* Codegenerator setup *}
-
-code_alias
-  "+" "Sum_Type.sum"
-  "Inr" "Sum_Type.Inr"
-  "Inl" "Sum_Type.Inl"
-
 end