src/HOL/Tools/datatype_realizer.ML
changeset 30364 577edc39b501
parent 30280 eb98b49ef835
child 30435 e62d6ecab6ad
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -168,7 +168,7 @@
     1.4          val Ts = map (typ_of_dtyp descr sorts) cargs;
     1.5          val frees = Name.variant_list ["P", "y"] (DatatypeProp.make_tnames Ts) ~~ Ts;
     1.6          val free_ts = map Free frees;
     1.7 -        val r = Free ("r" ^ NameSpace.base_name cname, Ts ---> rT)
     1.8 +        val r = Free ("r" ^ Long_Name.base_name cname, Ts ---> rT)
     1.9        in (r, list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
    1.10          (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
    1.11            HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $