src/Pure/more_thm.ML
changeset 31177 c39994cb152a
parent 31174 f1f1e9b53c81
child 31904 a86896359ca4
--- a/src/Pure/more_thm.ML	Sun May 17 07:17:39 2009 +0200
+++ b/src/Pure/more_thm.ML	Mon May 18 09:48:06 2009 +0200
@@ -70,7 +70,7 @@
   val assumptionK: string
   val definitionK: string
   val theoremK: string
-  val generated_theoremK : string
+  val generatedK : string
   val lemmaK: string
   val corollaryK: string
   val internalK: string
@@ -389,7 +389,7 @@
 val assumptionK = "assumption";
 val definitionK = "definition";
 val theoremK = "theorem";
-val generated_theoremK = "generated_theoremK"
+val generatedK = "generatedK"
 val lemmaK = "lemma";
 val corollaryK = "corollary";
 val internalK = Markup.internalK;