src/Pure/logic.ML
changeset 30364 577edc39b501
parent 30280 eb98b49ef835
child 30554 73f8bd5f0af8
--- a/src/Pure/logic.ML	Sun Mar 08 17:19:15 2009 +0100
+++ b/src/Pure/logic.ML	Sun Mar 08 17:26:14 2009 +0100
@@ -230,7 +230,7 @@
 (* class relations *)
 
 fun name_classrel (c1, c2) =
-  NameSpace.base_name c1 ^ "_" ^ NameSpace.base_name c2;
+  Long_Name.base_name c1 ^ "_" ^ Long_Name.base_name c2;
 
 fun mk_classrel (c1, c2) = mk_inclass (Term.aT [c1], c2);
 
@@ -243,8 +243,8 @@
 (* type arities *)
 
 fun name_arities (t, _, S) =
-  let val b = NameSpace.base_name t
-  in S |> map (fn c => NameSpace.base_name c ^ "_" ^ b) end;
+  let val b = Long_Name.base_name t
+  in S |> map (fn c => Long_Name.base_name c ^ "_" ^ b) end;
 
 fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));