src/Pure/Proof/proof_rewrite_rules.ML
changeset 22662 3e492ba59355
parent 22280 a20a203c8f41
child 23178 07ba6b58b3d2
     1.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Apr 13 15:43:25 2007 +0200
     1.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Apr 13 16:40:16 2007 +0200
     1.3 @@ -187,7 +187,7 @@
     1.4    in rew' end;
     1.5  
     1.6  fun rprocs b = [("Pure/meta_equality", rew b)];
     1.7 -val _ = Context.add_setup (Proofterm.add_prf_rprocs (rprocs false));
     1.8 +val _ = Context.add_setup (fold Proofterm.add_prf_rproc (rprocs false));
     1.9  
    1.10  
    1.11  (**** apply rewriting function to all terms in proof ****)