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

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

    70 axioms t_eq: "EQUIV Rt"

    70 axioms t_eq: "EQUIV Rt"

    71 

    71 

    72 quotient qt = "t" / "Rt"

    72 quotient qt = "t" / "Rt"

    73   by (rule t_eq)

    73   by (rule t_eq)

    75 

    74 

    76 ML {*

    75 ML {*

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

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

    78   |> fst

    77   |> fst

    79   |> Syntax.string_of_term @{context}

    78   |> Syntax.string_of_term @{context}