src/Pure/pure_thy.scala

--- a/src/Pure/pure_thy.scala	Sun Jul 21 12:28:02 2019 +0200
+++ b/src/Pure/pure_thy.scala	Sun Jul 21 15:19:07 2019 +0200
@@ -22,16 +22,16 @@
   val TYPE: String = "Pure.type"
 
 
-  /* proof terms (abstract syntax) */
+  /* abstract syntax for proof terms */
 
-  val PROOF: String = "proof"
+  val PROOF: String = "Pure.proof"
 
-  val APPT: String = "Appt"
-  val APPP: String = "AppP"
-  val ABST: String = "Abst"
-  val ABSP: String = "AbsP"
-  val HYP: String = "Hyp"
-  val ORACLE: String = "Oracle"
-  val OFCLASS: String = "OfClass"
-  val MINPROOF: String = "MinProof"
+  val APPT: String = "Pure.Appt"
+  val APPP: String = "Pure.AppP"
+  val ABST: String = "Pure.Abst"
+  val ABSP: String = "Pure.AbsP"
+  val HYP: String = "Pure.Hyp"
+  val ORACLE: String = "Pure.Oracle"
+  val OFCLASS: String = "Pure.OfClass"
+  val MINPROOF: String = "Pure.MinProof"
 }