# HG changeset patch
# User berghofe
# Date 1090253746 -7200
# Node ID a43d771c18acba40fcf00f7182963365b7a71e2d
# Parent  8049f217428e6c111d4948e057ce5081a8b0f9ce
Moved code generator setup for lists to List.thy

diff -r 8049f217428e -r a43d771c18ac src/HOL/Main.thy
--- a/src/HOL/Main.thy	Mon Jul 19 18:14:57 2004 +0200
+++ b/src/HOL/Main.thy	Mon Jul 19 18:15:46 2004 +0200
@@ -17,7 +17,6 @@
 types_code
   "bool"  ("bool")
   "*"     ("(_ */ _)")
-  "list"  ("_ list")
 
 consts_code
   "True"    ("true")
@@ -31,9 +30,6 @@
   "fst"     ("fst")
   "snd"     ("snd")
 
-  "Nil"     ("[]")
-  "Cons"    ("(_ ::/ _)")
-
   "wfrec"   ("wf'_rec?")
 
 quickcheck_params [default_type = int]
@@ -42,7 +38,6 @@
 fun wf_rec f x = f (wf_rec f) x;
 
 fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
-val term_of_list = HOLogic.mk_list;
 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);
@@ -65,10 +60,6 @@
 
 fun gen_bool i = one_of [false, true];
 
-fun gen_list' aG i j = frequency
-  [(i, fn () => aG j :: gen_list' aG (i-1) j), (1, fn () => [])] ()
-and gen_list aG i = gen_list' aG i i;
-
 fun gen_int i = one_of [~1, 1] * random_range 0 i;
 
 fun gen_id_42 aG bG i = (aG i, bG i);