src/HOL/Nominal/nominal_fresh_fun.ML
changeset 59586 ddf6deaadfe8
parent 59582 0fbed69ff081
child 59621 291934bac95e
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Mar 04 20:50:20 2015 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Mar 04 22:05:01 2015 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4    let
     1.5      val thy = Thm.theory_of_thm st;
     1.6      val cgoal = nth (cprems_of st) (i - 1);
     1.7 -    val {maxidx, ...} = Thm.rep_cterm cgoal;
     1.8 +    val maxidx = Thm.maxidx_of_cterm cgoal;
     1.9      val j = maxidx + 1;
    1.10      val tyinst' = map (apfst (Logic.incr_tvar j)) tyinst;
    1.11      val ps = Logic.strip_params (Thm.term_of cgoal);