equal
deleted
inserted
replaced
445 *) |
445 *) |
446 |
446 |
447 local |
447 local |
448 |
448 |
449 fun contract_lhs th = |
449 fun contract_lhs th = |
450 Thm.transitive (Thm.symmetric (beta_eta_conversion |
450 Thm.transitive (Thm.symmetric (beta_eta_conversion (#1 (Thm.dest_equals (Thm.cprop_of th))))) th; |
451 (fst (Thm.dest_equals (Thm.cprop_of th))))) th; |
|
452 |
451 |
453 fun var_args ct = |
452 fun var_args ct = |
454 (case try Thm.dest_comb ct of |
453 (case try Thm.dest_comb ct of |
455 SOME (f, arg) => |
454 SOME (f, arg) => |
456 (case Thm.term_of arg of |
455 (case Thm.term_of arg of |