src/HOL/Nominal/nominal_fresh_fun.ML
changeset 46219 426ed18eba43
parent 44121 44adaa6db327
child 47060 e2741ec9ae36
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Jan 14 20:05:58 2012 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Jan 14 21:16:15 2012 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4      val Ts = map snd ps;
     1.5      val tinst' = map (fn (t, u) =>
     1.6        (head_of (Logic.incr_indexes (Ts, j) t),
     1.7 -       list_abs (ps, u))) tinst;
     1.8 +       fold_rev Term.abs ps u)) tinst;
     1.9      val th' = instf
    1.10        (map (pairself (ctyp_of thy)) tyinst')
    1.11        (map (pairself (cterm_of thy)) tinst')
    1.12 @@ -155,9 +155,10 @@
    1.13     let val vars' = Misc_Legacy.term_vars (prop_of st);
    1.14         val thy = theory_of_thm st;
    1.15     in case subtract (op =) vars vars' of
    1.16 -     [x] => Seq.single (Thm.instantiate ([],[(cterm_of thy x,cterm_of thy (list_abs (params,Bound 0)))]) st)
    1.17 +     [x] =>
    1.18 +      Seq.single (Thm.instantiate ([],[(cterm_of thy x,cterm_of thy (fold_rev Term.abs params (Bound 0)))]) st)
    1.19      | _ => error "fresh_fun_simp: Too many variables, please report."
    1.20 -  end
    1.21 +   end
    1.22    in
    1.23    ((fn st =>
    1.24    let