1.1 --- a/src/HOL/Tools/record.ML	Sat Jan 15 15:29:17 2011 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Jan 15 15:37:49 2011 +0100
     1.3 @@ -1802,7 +1802,7 @@
     1.4            ((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, termifyT T'))) params)
     1.5          tc @{typ Random.seed} (SOME Tm, @{typ Random.seed});
     1.6      val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
     1.7 -  in 
     1.8 +  in
     1.9      thy
    1.10      |> Class.instantiation ([tyco], vs, @{sort random})
    1.11      |> `(fn lthy => Syntax.check_term lthy eq)
    1.12 @@ -1815,11 +1815,14 @@
    1.13    let
    1.14      val algebra = Sign.classes_of thy;
    1.15      val has_inst = can (Sorts.mg_domain algebra ext_tyco) @{sort random};
    1.16 -  in if has_inst then thy
    1.17 -    else case Quickcheck_Generators.perhaps_constrain thy (map (rpair @{sort random}) Ts) vs
    1.18 -     of SOME constrain => instantiate_random_record ext_tyco (map constrain vs) extN
    1.19 -          ((map o map_atyps) (fn TFree v => TFree (constrain v)) Ts) thy
    1.20 -      | NONE => thy
    1.21 +  in
    1.22 +    if has_inst then thy
    1.23 +    else
    1.24 +      (case Quickcheck_Generators.perhaps_constrain thy (map (rpair @{sort random}) Ts) vs of
    1.25 +        SOME constrain =>
    1.26 +          instantiate_random_record ext_tyco (map constrain vs) extN
    1.27 +            ((map o map_atyps) (fn TFree v => TFree (constrain v)) Ts) thy
    1.28 +      | NONE => thy)
    1.29    end;
    1.30  
    1.31  fun add_code ext_tyco vs extT ext simps inject thy =
    1.32 @@ -1837,7 +1840,7 @@
    1.33      fun mk_eq_refl thy =
    1.34        @{thm equal_refl}
    1.35        |> Thm.instantiate
    1.36 -        ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
    1.37 +        ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
    1.38        |> AxClass.unoverload thy;
    1.39    in
    1.40      thy
    1.41 @@ -1846,11 +1849,12 @@
    1.42      |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
    1.43      |> `(fn lthy => Syntax.check_term lthy eq)
    1.44      |-> (fn eq => Specification.definition
    1.45 -         (NONE, (Attrib.empty_binding, eq)))
    1.46 +          (NONE, (Attrib.empty_binding, eq)))
    1.47      |-> (fn (_, (_, eq_def)) =>
    1.48         Class.prove_instantiation_exit_result Morphism.thm
    1.49 -         (fn _ => fn eq_def => tac eq_def) eq_def)
    1.50 -    |-> (fn eq_def => fn thy => thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
    1.51 +          (fn _ => fn eq_def => tac eq_def) eq_def)
    1.52 +    |-> (fn eq_def => fn thy =>
    1.53 +          thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
    1.54      |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
    1.55      |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
    1.56    end;