equal
deleted
inserted
replaced
220 fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons); |
220 fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons); |
221 |
221 |
222 val thy'' = thy''' |> |
222 val thy'' = thy''' |> |
223 Domain_Isomorphism.domain_isomorphism |
223 Domain_Isomorphism.domain_isomorphism |
224 (map (fn ((vs, dname, mx, _), eq) => |
224 (map (fn ((vs, dname, mx, _), eq) => |
225 (map fst vs, dname, mx, mk_eq_typ eq)) |
225 (map fst vs, dname, mx, mk_eq_typ eq, NONE)) |
226 (eqs''' ~~ eqs')) |
226 (eqs''' ~~ eqs')) |
227 |
227 |
228 val thy' = thy'' |> Domain_Syntax.add_syntax true comp_dnam eqs'; |
228 val thy' = thy'' |> Domain_Syntax.add_syntax true comp_dnam eqs'; |
229 val dts = map (Type o fst) eqs'; |
229 val dts = map (Type o fst) eqs'; |
230 val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs'; |
230 val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs'; |