src/CTT/rew.ML
changeset 17496 26535df536ae
parent 1459 d12da312eff4
child 19761 5cd82054c2c6
     1.1 --- a/src/CTT/rew.ML	Tue Sep 20 08:20:22 2005 +0200
     1.2 +++ b/src/CTT/rew.ML	Tue Sep 20 08:21:49 2005 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  (*Make list of ProdE RS ProdE ... RS ProdE RS EqE
     1.5    for using assumptions as rewrite rules*)
     1.6  fun peEs 0 = []
     1.7 -  | peEs n = EqE :: map (apl(ProdE, op RS)) (peEs (n-1));
     1.8 +  | peEs n = EqE :: map (curry (op RS) ProdE) (peEs (n-1));
     1.9  
    1.10  (*Tactic used for proving conditions for the cond_rls*)
    1.11  val prove_cond_tac = eresolve_tac (peEs 5);