1.1 --- a/src/HOL/Tools/quickcheck_generators.ML Sun Jun 14 09:11:51 2009 +0200
1.2 +++ b/src/HOL/Tools/quickcheck_generators.ML Sun Jun 14 09:13:59 2009 +0200
1.3 @@ -370,13 +370,9 @@
1.4 can (Sorts.mg_domain algebra tyco) @{sort random}) tycos;
1.5 in if has_inst then thy
1.6 else case perhaps_constrain thy (random_insts @ term_of_insts) raw_vs
1.7 - of SOME constrain => (mk_random_datatype descr
1.8 + of SOME constrain => mk_random_datatype descr
1.9 (map constrain raw_vs) tycos (names, auxnames)
1.10 ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
1.11 - (*FIXME ephemeral handles*)
1.12 - handle e as TERM (msg, ts) => (tracing (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts)); raise e)
1.13 - | e as TYPE (msg, _, _) => (tracing msg; raise e)
1.14 - | e as ERROR msg => (tracing msg; raise e))
1.15 | NONE => thy
1.16 end;
1.17