src/Pure/Isar/locale.ML
changeset 28941 128459bd72d2
parent 28940 df0cb410be35
child 28950 b2db06eb214d
     1.1 --- a/src/Pure/Isar/locale.ML	Mon Dec 01 16:02:57 2008 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Mon Dec 01 19:41:16 2008 +0100
     1.3 @@ -947,8 +947,8 @@
     1.4          val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params;
     1.5          val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
     1.6          val (lprfx, pprfx) = param_prefix name params;
     1.7 -        val add_prefices = pprfx <> "" ? Name.add_prefix false pprfx
     1.8 -          #> Name.add_prefix false lprfx;
     1.9 +        val add_prefices = pprfx <> "" ? Binding.add_prefix false pprfx
    1.10 +          #> Binding.add_prefix false lprfx;
    1.11          val elem_morphism =
    1.12            Element.rename_morphism ren $>
    1.13            Morphism.name_morphism add_prefices $>
    1.14 @@ -1634,10 +1634,10 @@
    1.15  
    1.16  fun name_morph phi_name (lprfx, pprfx) b =
    1.17    b
    1.18 -  |> (if not (Name.is_nothing b) andalso pprfx <> ""
    1.19 -        then Name.add_prefix false pprfx else I)
    1.20 -  |> (if not (Name.is_nothing b)
    1.21 -        then Name.add_prefix false lprfx else I)
    1.22 +  |> (if not (Binding.is_nothing b) andalso pprfx <> ""
    1.23 +        then Binding.add_prefix false pprfx else I)
    1.24 +  |> (if not (Binding.is_nothing b)
    1.25 +        then Binding.add_prefix false lprfx else I)
    1.26    |> phi_name;
    1.27  
    1.28  fun inst_morph thy phi_name param_prfx insts prems eqns export =
    1.29 @@ -2442,11 +2442,11 @@
    1.30    end;
    1.31  
    1.32  fun standard_name_morph interp_prfx b =
    1.33 -  if Name.is_nothing b then b
    1.34 -  else Name.map_prefix (fn ((lprfx, _) :: pprfx) =>
    1.35 -    fold (Name.add_prefix false o fst) pprfx
    1.36 -    #> interp_prfx <> "" ? Name.add_prefix true interp_prfx
    1.37 -    #> Name.add_prefix false lprfx
    1.38 +  if Binding.is_nothing b then b
    1.39 +  else Binding.map_prefix (fn ((lprfx, _) :: pprfx) =>
    1.40 +    fold (Binding.add_prefix false o fst) pprfx
    1.41 +    #> interp_prfx <> "" ? Binding.add_prefix true interp_prfx
    1.42 +    #> Binding.add_prefix false lprfx
    1.43    ) b;
    1.44  
    1.45  in