# HG changeset patch
# User wenzelm
# Date 1563901648 -7200
# Node ID 3c9f6aad092fd6220d6e2cc822412f396435b68d
# Parent  65bbef66e2ec82161f3ae5781eddec27ab825fc6
discontinued Proofterm.Promise (cf. 725438ceae7c);

diff -r 65bbef66e2ec -r 3c9f6aad092f src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Tue Jul 23 19:04:56 2019 +0200
+++ b/src/Doc/Implementation/Logic.thy	Tue Jul 23 19:07:28 2019 +0200
@@ -1191,8 +1191,8 @@
   \<^descr> Type \<^ML_type>\<open>proof\<close> represents proof terms; this is a datatype with
   constructors @{index_ML Abst}, @{index_ML AbsP}, @{index_ML_op "%"},
   @{index_ML_op "%%"}, @{index_ML PBound}, @{index_ML MinProof}, @{index_ML
-  Hyp}, @{index_ML PAxm}, @{index_ML Oracle}, @{index_ML Promise}, @{index_ML
-  PThm} as explained above. %FIXME OfClass (!?)
+  Hyp}, @{index_ML PAxm}, @{index_ML Oracle}, @{index_ML PThm} as explained
+  above. %FIXME OfClass (!?)
 
   \<^descr> Type \<^ML_type>\<open>proof_body\<close> represents the nested proof information of a
   named theorem, consisting of a digest of oracles and named theorem over some