8 

     9 ML {*

    10 let

    11    val parser = Args.context -- Scan.lift Args.name_source

    12    fun term_pat (ctxt, str) =

    13       str |> ProofContext.read_term_pattern ctxt

    14           |> ML_Syntax.print_term

    15           |> ML_Syntax.atomic

    16 in

    17    ML_Antiquote.inline "term_pat" (parser >> term_pat)

    18 end

    19 *}

    20 

    21 ML {*

    22 fun pretty_helper aux env =

    23   env |> Vartab.dest

    24       |> map ((fn (s1, s2) => s1 ^ " := " ^ s2) o aux)

    25       |> commas

    26       |> enclose "[" "]"

    27       |> tracing

    28 *}

    29 

    30 ML {*

    31 fun pretty_env ctxt env =

    32 let

    33    fun get_trms (v, (T, t)) = (Var (v, T), t)

    34    val print = pairself (Syntax.string_of_term ctxt)

    35 in

    36    pretty_helper (print o get_trms) env

    37 end

    38 *}

    39 

    40 ML {* val pat = @{term_pat "\<lambda>(x::'a list \<Rightarrow> bool). 

    41          (?f)

    42          ((g::('a list \<Rightarrow> bool)\<Rightarrow>'a list \<Rightarrow> bool) x)"} *}

    43 ML {* val trm = @{term_pat "\<lambda>(x::'a list \<Rightarrow> bool). 

    44           (f::('a List.list \<Rightarrow> bool) \<Rightarrow> ('a List.list \<Rightarrow> bool) \<Rightarrow> 'b)

    45           ((g::('a list \<Rightarrow> bool)\<Rightarrow>'a list \<Rightarrow> bool) x) ((g::('a list \<Rightarrow> bool)\<Rightarrow>'a list \<Rightarrow> bool) x)"} *}

    46 

    47 ML {* val univ = let

    48   val init = Envir.empty 0

    49 in

    50   Unify.unifiers (@{theory}, init, [(pat, trm)])

    51 end

    52 *}

    53 

    54 ML {* val SOME ((u1, _), next) = Seq.pull univ *}

    55 ML {* val NEXT = Seq.pull next *}

    56 

    57 ML {* show_types := true *}

    58 ML {* pretty_env @{context} (Envir.term_env u1); *}