tuned

--- 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