src/Pure/more_thm.ML
changeset 42440 5e7a7343ab11
parent 42375 774df7c59508
child 42473 aca720fb3936
--- a/src/Pure/more_thm.ML	Wed Apr 20 22:57:29 2011 +0200
+++ b/src/Pure/more_thm.ML	Thu Apr 21 12:56:27 2011 +0200
@@ -87,7 +87,6 @@
   val has_name_hint: thm -> bool
   val get_name_hint: thm -> string
   val put_name_hint: string -> thm -> thm
-  val definitionK: string
   val theoremK: string
   val lemmaK: string
   val corollaryK: string
@@ -450,7 +449,6 @@
 
 (* theorem kinds *)
 
-val definitionK = "definition";
 val theoremK = "theorem";
 val lemmaK = "lemma";
 val corollaryK = "corollary";