143 Pretty.commas (map prt_const' (sort_wrt #1 rhs))); |
143 Pretty.commas (map prt_const' (sort_wrt #1 rhs))); |
144 |
144 |
145 fun pretty_restrict (const, name) = |
145 fun pretty_restrict (const, name) = |
146 Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]); |
146 Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]); |
147 |
147 |
148 val axioms = (Theory.axiom_space thy, Theory.axiom_table thy); |
|
149 val defs = Theory.defs_of thy; |
148 val defs = Theory.defs_of thy; |
150 val {restricts, reducts} = Defs.dest defs; |
149 val {restricts, reducts} = Defs.dest defs; |
151 val tsig = Sign.tsig_of thy; |
150 val tsig = Sign.tsig_of thy; |
152 val consts = Sign.consts_of thy; |
151 val consts = Sign.consts_of thy; |
153 val {constants, constraints} = Consts.dest consts; |
152 val {const_space, constants, constraints} = Consts.dest consts; |
154 val extern_const = Name_Space.extern ctxt (#1 constants); |
153 val extern_const = Name_Space.extern ctxt const_space; |
155 val {classes, default, types, ...} = Type.rep_tsig tsig; |
154 val {classes, default, types, ...} = Type.rep_tsig tsig; |
156 val (class_space, class_algebra) = classes; |
155 val (class_space, class_algebra) = classes; |
157 val classes = Sorts.classes_of class_algebra; |
156 val classes = Sorts.classes_of class_algebra; |
158 val arities = Sorts.arities_of class_algebra; |
157 val arities = Sorts.arities_of class_algebra; |
159 |
158 |
160 val clsses = |
159 val clsses = |
161 Name_Space.dest_table ctxt (class_space, |
160 Name_Space.dest_table' ctxt class_space |
162 Symtab.make (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes))); |
161 (Symtab.make (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes))) |
163 val tdecls = Name_Space.dest_table ctxt types; |
162 |> map (apfst #1); |
164 val arties = Name_Space.dest_table ctxt (Type.type_space tsig, arities); |
163 val tdecls = Name_Space.dest_table ctxt types |> map (apfst #1); |
|
164 val arties = Name_Space.dest_table' ctxt (Type.type_space tsig) arities |> map (apfst #1); |
165 |
165 |
166 fun prune_const c = not verbose andalso Consts.is_concealed consts c; |
166 fun prune_const c = not verbose andalso Consts.is_concealed consts c; |
167 val cnsts = Name_Space.extern_table ctxt (#1 constants, |
167 val cnsts = |
168 Symtab.make (filter_out (prune_const o fst) (Symtab.dest (#2 constants)))); |
168 Name_Space.extern_table' ctxt const_space |
|
169 (Symtab.make (filter_out (prune_const o fst) (Symtab.dest constants))); |
169 |
170 |
170 val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts; |
171 val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts; |
171 val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts; |
172 val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts; |
172 val cnstrs = Name_Space.extern_table ctxt constraints; |
173 val cnstrs = Name_Space.extern_table' ctxt const_space constraints; |
173 |
174 |
174 val axms = Name_Space.extern_table ctxt axioms; |
175 val axms = Name_Space.extern_table ctxt (Theory.axiom_table thy); |
175 |
176 |
176 val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts |
177 val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts |
177 |> map (fn (lhs, rhs) => |
178 |> map (fn (lhs, rhs) => |
178 (apfst extern_const lhs, map (apfst extern_const) (filter_out (prune_const o fst) rhs))) |
179 (apfst extern_const lhs, map (apfst extern_const) (filter_out (prune_const o fst) rhs))) |
179 |> sort_wrt (#1 o #1) |
180 |> sort_wrt (#1 o #1) |