src/HOL/Tools/datatype_realizer.ML
changeset 30280 eb98b49ef835
parent 30190 479806475f3c
child 30364 577edc39b501
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Thu Mar 05 11:58:53 2009 +0100
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Thu Mar 05 12:08:00 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 cname, Ts ---> rT)
     1.8 +        val r = Free ("r" ^ NameSpace.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) $