# HG changeset patch
# User haftmann
# Date 1140431886 -3600
# Node ID 1f6112de1d0f7309f392e9a2875df2a71ac5e260
# Parent  4bda27adcd2efbb2673fd874aa32f8465940dfd3
slight code generator serialization improvements

diff -r 4bda27adcd2e -r 1f6112de1d0f src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Mon Feb 20 11:37:18 2006 +0100
+++ b/src/HOL/Datatype.thy	Mon Feb 20 11:38:06 2006 +0100
@@ -235,6 +235,12 @@
     ml (target_atom "(__,/ __)")
     haskell (target_atom "(__,/ __)")
 
+lemma [code]:
+  "fst (x, y) = x" by simp
+
+lemma [code]:
+  "snd (x, y) = y" by simp
+
 code_syntax_const
   1 :: "nat"
     ml ("{*Suc 0*}")
diff -r 4bda27adcd2e -r 1f6112de1d0f src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon Feb 20 11:37:18 2006 +0100
+++ b/src/HOL/Product_Type.thy	Mon Feb 20 11:38:06 2006 +0100
@@ -785,27 +785,11 @@
   "fst" "Product_Type.fst"
   "snd" "Product_Type.snd"
 
-code_primconst fst
-ml {*
-fun `_` (x, y) = x;
-*}
-
-code_primconst snd
-ml {*
-fun `_` (x, y) = y;
-*}
-
 code_syntax_tyco
   *
     ml (infix 2 "*")
     haskell (target_atom "(__,/ __)")
 
-code_syntax_const
-  fst
-    haskell (target_atom "fst")
-  snd
-    haskell (target_atom "snd")
-
 ML {*
 
 fun strip_abs_split 0 t = ([], t)
diff -r 4bda27adcd2e -r 1f6112de1d0f src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Mon Feb 20 11:37:18 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Mon Feb 20 11:38:06 2006 +0100
@@ -159,12 +159,11 @@
   val ord = prod_ord string_ord (prod_ord Term.typ_ord Term.typ_ord);
   fun mk (thy, deftab) ((c, (ty_decl, ty)), i) =
     let
-      val thyname = if c = "op ="
-        then
-          (NameSpace.drop_base o alias_get thy o fst o dest_Type o hd o fst o strip_type) ty
-        else (the o get_first
+      val thyname = case (get_first
           (fn (ty', (_, thyname)) => if eq_typ thy (ty, ty') then SOME thyname else NONE)
-          o the o Symtab.lookup deftab) c;
+            o these o Symtab.lookup deftab) c
+        of SOME thyname => thyname
+         | _ => (NameSpace.drop_base o alias_get thy o fst o dest_Type o hd o fst o strip_type) ty
       val c' = idf_of_name thy nsp_overl c;
       val c'' = NameSpace.append thyname (NameSpace.append nsp_overl (NameSpace.base c'));
       fun mangle (Type (tyco, tys)) =
diff -r 4bda27adcd2e -r 1f6112de1d0f src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Mon Feb 20 11:37:18 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Mon Feb 20 11:38:06 2006 +0100
@@ -976,7 +976,7 @@
       "import", "default", "forall", "let", "in", "class", "qualified", "data",
       "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
     ] @ [
-      "Bool", "fst", "snd", "Integer", "True", "False", "negate"
+      "Bool", "Integer", "True", "False", "negate"
     ];
     fun hs_from_module imps ((_, name), ps) =
       (Pretty.chunks) (