changeset 60329 | e85ed7a36b2f |
parent 59621 | 291934bac95e |
child 60334 | 63f25a1adcfc |
--- a/src/HOL/Tools/TFL/rules.ML Mon Jun 01 13:35:16 2015 +0200 +++ b/src/HOL/Tools/TFL/rules.ML Mon Jun 01 13:46:23 2015 +0200 @@ -636,7 +636,7 @@ in (strip_aabs used f,args) end; -fun pbeta_redex M n = can (Utils.C (dest_pbeta_redex []) n) M; +fun pbeta_redex M n = can (fn t => dest_pbeta_redex [] t n) M; fun dest_impl tm = let val ants = Logic.strip_imp_prems tm