src/Pure/logic.ML
changeset 30364 577edc39b501
parent 30280 eb98b49ef835
child 30554 73f8bd5f0af8
     1.1 --- a/src/Pure/logic.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/Pure/logic.ML	Sun Mar 08 17:26:14 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_name c1 ^ "_" ^ NameSpace.base_name c2;
     1.8 +  Long_Name.base_name c1 ^ "_" ^ Long_Name.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_name t
    1.17 -  in S |> map (fn c => NameSpace.base_name c ^ "_" ^ b) end;
    1.18 +  let val b = Long_Name.base_name t
    1.19 +  in S |> map (fn c => Long_Name.base_name c ^ "_" ^ b) end;
    1.20  
    1.21  fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
    1.22