src/Pure/more_thm.ML
changeset 33644 5266a72e0889
parent 33643 b275f26a638b
child 33666 e49bfeb0d822
--- a/src/Pure/more_thm.ML	Thu Nov 12 22:02:11 2009 +0100
+++ b/src/Pure/more_thm.ML	Thu Nov 12 22:29:54 2009 +0100
@@ -84,8 +84,6 @@
   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
@@ -413,8 +411,6 @@
 
 (* theorem kinds *)
 
-val axiomK = "axiom";
-val assumptionK = "assumption";
 val definitionK = "definition";
 val theoremK = "theorem";
 val generatedK = "generatedK"