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