4 

     5 (* test for get_fun *)

     6 datatype t =

     7    vr "string"

     8  | ap "t list"

     9  | lm "string" "t"

    10 

    11 consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"

    12 axioms t_eq: "EQUIV Rt"

    13 

    14 quotient qt = "t" / "Rt"

    15     by (rule t_eq)

    16 

    17 ML {*

    18 get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}

    19  |> fst

    20  |> Syntax.string_of_term @{context}

    21  |> writeln

    22 *}

    23 

    24 ML {*

    25 get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"}

    26  |> fst

    27  |> Syntax.string_of_term @{context}

    28  |> writeln

    29 *}

    30 

    31 ML {*

    32 get_fun absF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}

    33  |> fst

    34  |> Syntax.pretty_term @{context}

    35  |> Pretty.string_of

    36  |> writeln

    37 *}

    38 (* end test get_fun *)

    39