changeset 41928 | 05abcee548a1 |
parent 41926 | b09a67a3dc1e |
child 42086 | 74bf78db0d87 |
--- 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 Random_Generators.perhaps_constrain thy (map (rpair @{sort random}) Ts) vs of + (case Quickcheck_Common.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