equal
deleted
inserted
replaced
1270 fun C f x y = f y x; |
1270 fun C f x y = f y x; |
1271 (* FIXME : This is very bad!!!*) |
1271 (* FIXME : This is very bad!!!*) |
1272 fun subst_conv eqs t = |
1272 fun subst_conv eqs t = |
1273 let |
1273 let |
1274 val t' = fold (Thm.cabs o Thm.lhs_of) eqs t |
1274 val t' = fold (Thm.cabs o Thm.lhs_of) eqs t |
1275 in Conv.fconv_rule (Thm.beta_conversion true) (fold (C combination) eqs (reflexive t')) |
1275 in Conv.fconv_rule (Thm.beta_conversion true) (fold (C Thm.combination) eqs (Thm.reflexive t')) |
1276 end |
1276 end |
1277 |
1277 |
1278 (* A wrapper that tries to substitute away variables first. *) |
1278 (* A wrapper that tries to substitute away variables first. *) |
1279 |
1279 |
1280 local |
1280 local |