tuned
authorhaftmann
Thu Aug 19 11:13:07 2010 +0200 (2010-08-19)
changeset 38550925c4d7b291e
parent 38549 d0385f2764d8
child 38551 8ddfc68a3908
tuned
src/HOL/Tools/hologic.ML
     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