# HG changeset patch
# User berghofe
# Date 1102693709 -3600
# Node ID b93cdbac8f46918a9f16656edac91c947c3ea671
# Parent  a2c34e6ca4f8e5f06a81468e86b9beebb4f49e3f
Moved code generator setup for product type to Product_Type.thy

diff -r a2c34e6ca4f8 -r b93cdbac8f46 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Fri Dec 10 16:48:01 2004 +0100
+++ b/src/HOL/Main.thy	Fri Dec 10 16:48:29 2004 +0100
@@ -19,7 +19,6 @@
 
 types_code
   "bool"  ("bool")
-  "*"     ("(_ */ _)")
 
 consts_code
   "True"    ("true")
@@ -29,10 +28,6 @@
   "op &"    ("(_ andalso/ _)")
   "If"      ("(if _/ then _/ else _)")
 
-  "Pair"    ("(_,/ _)")
-  "fst"     ("fst")
-  "snd"     ("snd")
-
   "wfrec"   ("wf'_rec?")
 
 quickcheck_params [default_type = int]
@@ -42,7 +37,6 @@
 
 fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
 val term_of_int = HOLogic.mk_int;
-fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y;
 fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
 
 val eq_codegen_setup = [Codegen.add_codegen "eq_codegen"
@@ -65,8 +59,6 @@
 
 fun gen_int i = one_of [~1, 1] * random_range 0 i;
 
-fun gen_id_42 aG bG i = (aG i, bG i);
-
 fun gen_fun_type _ G i =
   let
     val f = ref (fn x => raise ERROR);