adapting record package to renaming of quickcheck's structures
authorbulwahn
Fri, 11 Mar 2011 15:21:13 +0100
changeset 41926 b09a67a3dc1e
parent 41925 4b9fdfd23752
child 41927 8759e9d043f9
adapting record package to renaming of quickcheck's structures
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 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