1969 val truncate_decl = (truncateN, rec_schemeT0 --> recT0); |
1969 val truncate_decl = (truncateN, rec_schemeT0 --> recT0); |
1970 |
1970 |
1971 |
1971 |
1972 (* prepare definitions *) |
1972 (* prepare definitions *) |
1973 |
1973 |
1974 (*record (scheme) type abbreviation*) |
|
1975 val recordT_specs = |
|
1976 [(Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), rec_schemeT0, NoSyn), |
|
1977 (binding, map #1 alphas, recT0, NoSyn)]; |
|
1978 |
|
1979 val ext_defs = ext_def :: map #ext_def parents; |
1974 val ext_defs = ext_def :: map #ext_def parents; |
1980 |
1975 |
1981 (*Theorems from the iso_tuple intros. |
1976 (*Theorems from the iso_tuple intros. |
1982 By unfolding ext_defs from r_rec0 we create a tree of constructor |
1977 By unfolding ext_defs from r_rec0 we create a tree of constructor |
1983 calls (many of them Pair, but others as well). The introduction |
1978 calls (many of them Pair, but others as well). The introduction |
2057 |
2052 |
2058 fun mk_defs () = |
2053 fun mk_defs () = |
2059 ext_thy |
2054 ext_thy |
2060 |> Sign.add_advanced_trfuns ([], [], advanced_print_translation, []) |
2055 |> Sign.add_advanced_trfuns ([], [], advanced_print_translation, []) |
2061 |> Sign.restore_naming thy |
2056 |> Sign.restore_naming thy |
2062 |> Sign.add_tyabbrs_i recordT_specs |
2057 |> Typedecl.abbrev_global (binding, map #1 alphas, NoSyn) recT0 |> snd |
|
2058 |> Typedecl.abbrev_global |
|
2059 (Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), NoSyn) rec_schemeT0 |> snd |
2063 |> Sign.qualified_path false binding |
2060 |> Sign.qualified_path false binding |
2064 |> fold (fn ((x, T), mx) => snd o Sign.declare_const ((Binding.name x, T), mx)) |
2061 |> fold (fn ((x, T), mx) => snd o Sign.declare_const ((Binding.name x, T), mx)) |
2065 (sel_decls ~~ (field_syntax @ [NoSyn])) |
2062 (sel_decls ~~ (field_syntax @ [NoSyn])) |
2066 |> fold (fn (x, T) => snd o Sign.declare_const ((Binding.name x, T), NoSyn)) |
2063 |> fold (fn (x, T) => snd o Sign.declare_const ((Binding.name x, T), NoSyn)) |
2067 (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl]) |
2064 (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl]) |