src/HOL/Tools/hologic.ML
changeset 38550 925c4d7b291e
parent 38548 dea0d2cca822
child 38555 bd6359ed1636
     1.1 --- a/src/HOL/Tools/hologic.ML	Thu Aug 19 11:02:14 2010 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Thu Aug 19 11:13:07 2010 +0200
     1.3 @@ -657,7 +657,9 @@
     1.4              $ t $ t', U)
     1.5    in fold_rev mk_clause clauses (t, U) |> fst end;
     1.6  
     1.7 -val code_numeralT = Type ("Code_Numeral.code_numeral", []);
     1.8 +
     1.9 +(* random seeds *)
    1.10 +
    1.11  val random_seedT = mk_prodT (code_numeralT, code_numeralT);
    1.12  
    1.13  fun mk_random T t = Const ("Quickcheck.random_class.random", code_numeralT