20 ML {*

    20 ML {*

    21 fun make_inst lhs t =

    21 fun make_inst lhs t =

    22   let

    22   let

    23     val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;

    23     val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;

    24     val _ $ (Abs (_, _, g)) = t;

    24     val _ $ (Abs (_, _, g)) = t;

    26       if incr_boundvars i u aconv t then Bound i

    27       if incr_boundvars i u aconv t then Bound i

    27       else (case t of

    28       else (case t of

    28         t1 $ t2 => mk_abs i t1 $ mk_abs i t2

    29         t1 $ t2 => mk_abs i t1 $ mk_abs i t2

    29       | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t')

    30       | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t')

    30       | Bound j => if i = j then error "make_inst" else t

    31       | Bound j => if i = j then error "make_inst" else t

    31       | _ => t);

    32       | _ => t);

    32   in (f, Abs ("x", T, mk_abs 0 g)) end;

    34   in (f, Abs ("x", T, mk_abs 0 g)) end;

    33 *}

    35 *}

    34 

    36 

    35 ML {* 

    37 ML {* 

    36   val trm1 = @{term_pat "(P::(nat\<Rightarrow>bool)\<Rightarrow>bool) (\<lambda>(x::nat). (?f ((g::nat\<Rightarrow>nat) x)))"}; 

    38   val trm1 = @{term_pat "(P::(nat\<Rightarrow>bool)\<Rightarrow>bool) (\<lambda>(x::nat). (?f ((g::nat\<Rightarrow>nat) x)))"};