src/Pure/more_thm.ML

   val def_name_optional: string -> string -> string
   val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding
   val has_name_hint: thm -> bool
   val get_name_hint: thm -> string
   val put_name_hint: string -> thm -> thm
-  val axiomK: string
-  val assumptionK: string
   val definitionK: string
   val theoremK: string
   val generatedK : string
   val lemmaK: string
   val corollaryK: string

 fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name);
 
 
 (* theorem kinds *)
 
-val axiomK = "axiom";
-val assumptionK = "assumption";
 val definitionK = "definition";
 val theoremK = "theorem";
 val generatedK = "generatedK"
 val lemmaK = "lemma";
 val corollaryK = "corollary";