diff -r 725438ceae7c -r ac570c179ee9 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Jul 23 12:07:50 2019 +0200
+++ b/src/Pure/proofterm.ML	Tue Jul 23 12:16:02 2019 +0200
@@ -1305,8 +1305,9 @@
 
 
 
-(** simple first order matching functions for terms and proofs **)
-(*see pattern.ML*)
+(** rewriting on proof terms **)
+
+(* simple first order matching functions for terms and proofs (see pattern.ML) *)
 
 exception PMatch;
 
@@ -1452,8 +1453,7 @@
   end;
 
 
-
-(** rewriting on proof terms **)
+(* rewrite proof *)
 
 val no_skel = PBound 0;
 val normal_skel = Hyp (Var ((Name.uu, 0), propT));
@@ -1545,8 +1545,7 @@
 fun rewrite_proof_notypes rews = rewrite_prf fst rews;
 
 
-
-(** theory data **)
+(* theory data *)
 
 structure Data = Theory_Data
 (