src/Pure/axclass.ML
changeset 30364 577edc39b501
parent 30344 10a67c5ddddb
child 30468 0cf8f536ef98
     1.1 --- a/src/Pure/axclass.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/Pure/axclass.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -158,7 +158,7 @@
     1.4  
     1.5  (* maintain instances *)
     1.6  
     1.7 -fun instance_name (a, c) = NameSpace.base_name c ^ "_" ^ NameSpace.base_name a;
     1.8 +fun instance_name (a, c) = Long_Name.base_name c ^ "_" ^ Long_Name.base_name a;
     1.9  
    1.10  val get_instances = #1 o #2 o AxClassData.get;
    1.11  val map_instances = AxClassData.map o apsnd o apfst;
    1.12 @@ -366,7 +366,7 @@
    1.13        | NONE => error ("Illegal type for instantiation of class parameter: "
    1.14          ^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T));
    1.15      val name_inst = instance_name (tyco, class) ^ "_inst";
    1.16 -    val c' = NameSpace.base_name c ^ "_" ^ NameSpace.base_name tyco;
    1.17 +    val c' = Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco;
    1.18      val T' = Type.strip_sorts T;
    1.19    in
    1.20      thy
    1.21 @@ -390,7 +390,7 @@
    1.22      val SOME tyco = inst_tyco_of thy (c, T);
    1.23      val (c', eq) = get_inst_param thy (c, tyco);
    1.24      val prop = Logic.mk_equals (Const (c', T), t);
    1.25 -    val name' = Thm.def_name_optional (NameSpace.base_name c ^ "_" ^ NameSpace.base_name tyco) name;
    1.26 +    val name' = Thm.def_name_optional (Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco) name;
    1.27    in
    1.28      thy
    1.29      |> Thm.add_def false false (Binding.name name', prop)