src/HOL/ex/Quickcheck_Generators.thy
changeset 30364 577edc39b501
parent 30280 eb98b49ef835
child 30945 0418e9bffbba
     1.1 --- a/src/HOL/ex/Quickcheck_Generators.thy	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/HOL/ex/Quickcheck_Generators.thy	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -138,7 +138,7 @@
     1.4      let
     1.5        val this_ty = Type (hd tycos, map TFree vs);
     1.6        val this_ty' = StateMonad.liftT (term_ty this_ty) @{typ seed};
     1.7 -      val random_name = NameSpace.base_name @{const_name random};
     1.8 +      val random_name = Long_Name.base_name @{const_name random};
     1.9        val random'_name = random_name ^ "_" ^ Class.type_name (hd tycos) ^ "'";
    1.10        fun random ty = Sign.mk_const thy (@{const_name random}, [ty]);
    1.11        val random' = Free (random'_name,