--- 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
(