1.1 --- a/src/Pure/axclass.ML	Sun Apr 25 19:09:37 2010 +0200
     1.2 +++ b/src/Pure/axclass.ML	Sun Apr 25 19:44:47 2010 +0200
     1.3 @@ -37,8 +37,6 @@
     1.4    val param_of_inst: theory -> string * string -> string
     1.5    val inst_of_param: theory -> string -> (string * string) option
     1.6    val thynames_of_arity: theory -> class * string -> string list
     1.7 -  val introN: string
     1.8 -  val axiomsN: string
     1.9  end;
    1.10  
    1.11  structure AxClass: AX_CLASS =
    1.12 @@ -64,10 +62,6 @@
    1.13  
    1.14  (* axclasses *)
    1.15  
    1.16 -val introN = "intro";
    1.17 -val superN = "super";
    1.18 -val axiomsN = "axioms";
    1.19 -
    1.20  datatype axclass = AxClass of
    1.21   {def: thm,
    1.22    intro: thm,
    1.23 @@ -563,9 +557,9 @@
    1.24        def_thy
    1.25        |> Sign.qualified_path true bconst
    1.26        |> PureThy.note_thmss ""
    1.27 -        [((Binding.name introN, []), [([Drule.export_without_context raw_intro], [])]),
    1.28 -         ((Binding.name superN, []), [(map Drule.export_without_context raw_classrel, [])]),
    1.29 -         ((Binding.name axiomsN, []),
    1.30 +        [((Binding.name "intro", []), [([Drule.export_without_context raw_intro], [])]),
    1.31 +         ((Binding.name "super", []), [(map Drule.export_without_context raw_classrel, [])]),
    1.32 +         ((Binding.name "axioms", []),
    1.33             [(map (fn th => Drule.export_without_context (class_triv RS th)) raw_axioms, [])])]
    1.34        ||> Sign.restore_naming def_thy;
    1.35