# HG changeset patch
# User wenzelm
# Date 1272217487 -7200
# Node ID 85d026788fced6b6d5005b6220b2e00ca161d52f
# Parent  8715343af626e423776de505bee187173d320397
simplified some private bindings;

diff -r 8715343af626 -r 85d026788fce src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sun Apr 25 19:09:37 2010 +0200
+++ b/src/Pure/axclass.ML	Sun Apr 25 19:44:47 2010 +0200
@@ -37,8 +37,6 @@
   val param_of_inst: theory -> string * string -> string
   val inst_of_param: theory -> string -> (string * string) option
   val thynames_of_arity: theory -> class * string -> string list
-  val introN: string
-  val axiomsN: string
 end;
 
 structure AxClass: AX_CLASS =
@@ -64,10 +62,6 @@
 
 (* axclasses *)
 
-val introN = "intro";
-val superN = "super";
-val axiomsN = "axioms";
-
 datatype axclass = AxClass of
  {def: thm,
   intro: thm,
@@ -563,9 +557,9 @@
       def_thy
       |> Sign.qualified_path true bconst
       |> PureThy.note_thmss ""
-        [((Binding.name introN, []), [([Drule.export_without_context raw_intro], [])]),
-         ((Binding.name superN, []), [(map Drule.export_without_context raw_classrel, [])]),
-         ((Binding.name axiomsN, []),
+        [((Binding.name "intro", []), [([Drule.export_without_context raw_intro], [])]),
+         ((Binding.name "super", []), [(map Drule.export_without_context raw_classrel, [])]),
+         ((Binding.name "axioms", []),
            [(map (fn th => Drule.export_without_context (class_triv RS th)) raw_axioms, [])])]
       ||> Sign.restore_naming def_thy;