src/Pure/axclass.ML
changeset 30280 eb98b49ef835
parent 30244 48543b307e99
child 30344 10a67c5ddddb
     1.1 --- a/src/Pure/axclass.ML	Thu Mar 05 11:58:53 2009 +0100
     1.2 +++ b/src/Pure/axclass.ML	Thu Mar 05 12:08:00 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 c ^ "_" ^ NameSpace.base a;
     1.8 +fun instance_name (a, c) = NameSpace.base_name c ^ "_" ^ NameSpace.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 @@ -367,7 +367,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 c ^ "_" ^ NameSpace.base tyco;
    1.17 +    val c' = NameSpace.base_name c ^ "_" ^ NameSpace.base_name tyco;
    1.18      val T' = Type.strip_sorts T;
    1.19    in
    1.20      thy
    1.21 @@ -391,7 +391,7 @@
    1.22      val (c', eq) = get_inst_param thy (c, tyco);
    1.23      val prop = Logic.mk_equals (Const (c', T), t);
    1.24      val name' = Thm.def_name_optional
    1.25 -      (NameSpace.base c ^ "_" ^ NameSpace.base tyco) name;
    1.26 +      (NameSpace.base_name c ^ "_" ^ NameSpace.base_name tyco) name;
    1.27    in
    1.28      thy
    1.29      |> Thm.add_def false false (Binding.name name', prop)