src/Pure/proofterm.ML

       | needed _ _ _ = [];
   in fn prf => #4 (shrink [] 0 prf) end;
 
 
 
-(** 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;
 
 fun flt (i: int) = filter (fn n => n < i);
 

       | (_, Abst _) =>  true
       | _ => false
   end;
 
 
-
-(** rewriting on proof terms **)
+(* rewrite proof *)
 
 val no_skel = PBound 0;
 val normal_skel = Hyp (Var ((Name.uu, 0), propT));
 
 fun rewrite_prf tymatch (rules, procs) prf =

   Sign.typ_match thy (f ()) tyenv handle Type.TYPE_MATCH => raise PMatch);
 
 fun rewrite_proof_notypes rews = rewrite_prf fst rews;
 
 
-
-(** theory data **)
+(* theory data *)
 
 structure Data = Theory_Data
 (
   type T =
     (stamp * (proof * proof)) list *