changeset 59586 | ddf6deaadfe8 |
parent 59582 | 0fbed69ff081 |
child 59621 | 291934bac95e |
--- a/src/HOL/Nominal/nominal_inductive.ML Wed Mar 04 20:50:20 2015 +0100 +++ b/src/HOL/Nominal/nominal_inductive.ML Wed Mar 04 22:05:01 2015 +0100 @@ -485,7 +485,7 @@ val (cf, ct) = Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th)); val arg_cong' = Drule.instantiate' - [SOME (Thm.ctyp_of_term ct)] + [SOME (Thm.ctyp_of_cterm ct)] [NONE, SOME ct, SOME cf] (arg_cong RS iffD2); val inst = Thm.first_order_match (ct, Thm.dest_arg (Thm.dest_arg (Thm.cprop_of th')))