diff -r 8759e9d043f9 -r 05abcee548a1 src/HOL/Tools/record.ML --- 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