author | bulwahn |
Fri, 11 Mar 2011 15:21:13 +0100 | |
changeset 41926 | b09a67a3dc1e |
parent 41925 | 4b9fdfd23752 |
child 41927 | 8759e9d043f9 |
--- a/src/HOL/Tools/record.ML Fri Mar 11 15:21:13 2011 +0100 +++ b/src/HOL/Tools/record.ML Fri Mar 11 15:21:13 2011 +0100 @@ -1835,7 +1835,7 @@ in if has_inst then thy else - (case Quickcheck_Generators.perhaps_constrain thy (map (rpair @{sort random}) Ts) vs of + (case Random_Generators.perhaps_constrain thy (map (rpair @{sort random}) Ts) vs of SOME constrain => instantiate_random_record ext_tyco (map constrain vs) extN ((map o map_atyps) (fn TFree v => TFree (constrain v)) Ts) thy