src/HOL/Nominal/nominal_thmdecls.ML
changeset 30364 577edc39b501
parent 30280 eb98b49ef835
child 30528 7173bf123335
     1.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -115,7 +115,7 @@
     1.4                 (Var (n,ty))) =>
     1.5               let
     1.6                  (* FIXME: this should be an operation the library *)
     1.7 -                val class_name = (NameSpace.map_base_name (fn s => "pt_"^s) tyatm)
     1.8 +                val class_name = (Long_Name.map_base_name (fn s => "pt_"^s) tyatm)
     1.9               in
    1.10                  if (Sign.of_sort thy (ty,[class_name]))
    1.11                  then [(pi,typi)]