--- 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*}")
--- 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)
--- 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)) =
--- 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) (