1640 ML {*

  1640 ML {*

  1641   mk_mapfun @{context} [@{typ_pat "?'a"}] @{typ_pat "(?'a list) * nat"}

  1641   mk_mapfun @{context} [@{typ_pat "?'a"}] @{typ_pat "(?'a list) * nat"}

  1642   |> Syntax.check_term @{context}

  1642   |> Syntax.check_term @{context}

  1643   |> fastype_of

  1643   |> fastype_of

  1644   |> Syntax.string_of_typ @{context}

  1644   |> Syntax.string_of_typ @{context}

  1646 *}

  1646 *}

  1647 

  1647 

  1648 ML {*

  1648 ML {*

  1649   mk_mapfun @{context} [@{typ_pat "?'a"}] @{typ_pat "(?'a list) * nat"}

  1649   mk_mapfun @{context} [@{typ_pat "?'a"}] @{typ_pat "(?'a list) * nat"}

  1650   |> Syntax.check_term @{context}

  1650   |> Syntax.check_term @{context}

  1651   |> Syntax.string_of_term @{context}

  1651   |> Syntax.string_of_term @{context}

  1652   |> warning

  1652   |> warning

  1653 *}

  1653 *}

  1654 

  1654 

  1655 ML {*

  1655 ML {*

  1656   absrep_fun AbsF @{context} (@{typ "('a list) list \<Rightarrow> 'a list"}, @{typ "('a fset) fset \<Rightarrow> 'a fset"})

  1666   absrep_fun AbsF @{context} (@{typ "('a list) list \<Rightarrow> 'a list"}, @{typ "('a fset) fset \<Rightarrow> 'a fset"})

  1657   |> Syntax.string_of_term @{context}

  1667   |> Syntax.string_of_term @{context}

  1658   |> writeln

  1668   |> writeln

  1659 *}

  1669 *}

  1660 

  1670