changeset 59586 | ddf6deaadfe8 |
parent 59582 | 0fbed69ff081 |
child 59621 | 291934bac95e |
--- a/src/HOL/Library/Code_Abstract_Nat.thy Wed Mar 04 20:50:20 2015 +0100 +++ b/src/HOL/Library/Code_Abstract_Nat.thy Wed Mar 04 22:05:01 2015 +0100 @@ -79,7 +79,7 @@ Thm.implies_elim (Conv.fconv_rule (Thm.beta_conversion true) (Drule.instantiate' - [SOME (Thm.ctyp_of_term ct)] [SOME (Thm.lambda cv ct), + [SOME (Thm.ctyp_of_cterm ct)] [SOME (Thm.lambda cv ct), SOME (Thm.lambda cv' (rhs_of thm)), NONE, SOME cv'] Suc_if_eq)) (Thm.forall_intr cv' thm) in