src/Pure/logic.ML
changeset 30280 eb98b49ef835
parent 29276 94b1ffec9201
child 30364 577edc39b501
     1.1 --- a/src/Pure/logic.ML	Thu Mar 05 11:58:53 2009 +0100
     1.2 +++ b/src/Pure/logic.ML	Thu Mar 05 12:08:00 2009 +0100
     1.3 @@ -230,7 +230,7 @@
     1.4  (* class relations *)
     1.5  
     1.6  fun name_classrel (c1, c2) =
     1.7 -  NameSpace.base c1 ^ "_" ^ NameSpace.base c2;
     1.8 +  NameSpace.base_name c1 ^ "_" ^ NameSpace.base_name c2;
     1.9  
    1.10  fun mk_classrel (c1, c2) = mk_inclass (Term.aT [c1], c2);
    1.11  
    1.12 @@ -243,8 +243,8 @@
    1.13  (* type arities *)
    1.14  
    1.15  fun name_arities (t, _, S) =
    1.16 -  let val b = NameSpace.base t
    1.17 -  in S |> map (fn c => NameSpace.base c ^ "_" ^ b) end;
    1.18 +  let val b = NameSpace.base_name t
    1.19 +  in S |> map (fn c => NameSpace.base_name c ^ "_" ^ b) end;
    1.20  
    1.21  fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
    1.22