1.1 --- a/src/HOL/Main.thy	Mon Jul 19 18:14:57 2004 +0200
     1.2 +++ b/src/HOL/Main.thy	Mon Jul 19 18:15:46 2004 +0200
     1.3 @@ -17,7 +17,6 @@
     1.4  types_code
     1.5    "bool"  ("bool")
     1.6    "*"     ("(_ */ _)")
     1.7 -  "list"  ("_ list")
     1.8  
     1.9  consts_code
    1.10    "True"    ("true")
    1.11 @@ -31,9 +30,6 @@
    1.12    "fst"     ("fst")
    1.13    "snd"     ("snd")
    1.14  
    1.15 -  "Nil"     ("[]")
    1.16 -  "Cons"    ("(_ ::/ _)")
    1.17 -
    1.18    "wfrec"   ("wf'_rec?")
    1.19  
    1.20  quickcheck_params [default_type = int]
    1.21 @@ -42,7 +38,6 @@
    1.22  fun wf_rec f x = f (wf_rec f) x;
    1.23  
    1.24  fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    1.25 -val term_of_list = HOLogic.mk_list;
    1.26  val term_of_int = HOLogic.mk_int;
    1.27  fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y;
    1.28  fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
    1.29 @@ -65,10 +60,6 @@
    1.30  
    1.31  fun gen_bool i = one_of [false, true];
    1.32  
    1.33 -fun gen_list' aG i j = frequency
    1.34 -  [(i, fn () => aG j :: gen_list' aG (i-1) j), (1, fn () => [])] ()
    1.35 -and gen_list aG i = gen_list' aG i i;
    1.36 -
    1.37  fun gen_int i = one_of [~1, 1] * random_range 0 i;
    1.38  
    1.39  fun gen_id_42 aG bG i = (aG i, bG i);