merged
authorhaftmann
Sun, 14 Jun 2009 09:13:59 +0200
changeset 3162940d775733848
parent 31627 bc2de3795756
parent 31628 28699098b5f3
child 31630 ea47e2b63588
child 31636 2f8ed0dca3bd
merged
     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