# HG changeset patch
# User haftmann
# Date 1282209187 -7200
# Node ID 925c4d7b291e4210b90ec41df017ee29ccfa70cb
# Parent  d0385f2764d893dc05b7001ac844c885b532c096
tuned

diff -r d0385f2764d8 -r 925c4d7b291e src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Thu Aug 19 11:02:14 2010 +0200
+++ b/src/HOL/Tools/hologic.ML	Thu Aug 19 11:13:07 2010 +0200
@@ -657,7 +657,9 @@
             $ t $ t', U)
   in fold_rev mk_clause clauses (t, U) |> fst end;
 
-val code_numeralT = Type ("Code_Numeral.code_numeral", []);
+
+(* random seeds *)
+
 val random_seedT = mk_prodT (code_numeralT, code_numeralT);
 
 fun mk_random T t = Const ("Quickcheck.random_class.random", code_numeralT