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