183 Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]); |
183 Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]); |
184 |
184 |
185 val axioms = (Theory.axiom_space thy, Theory.axiom_table thy); |
185 val axioms = (Theory.axiom_space thy, Theory.axiom_table thy); |
186 val defs = Theory.defs_of thy; |
186 val defs = Theory.defs_of thy; |
187 val {restricts, reducts} = Defs.dest defs; |
187 val {restricts, reducts} = Defs.dest defs; |
188 val {naming = _, syn = _, tsig, consts} = Sign.rep_sg thy; |
188 val tsig = Sign.tsig_of thy; |
|
189 val consts = Sign.consts_of thy; |
189 val {constants, constraints} = Consts.dest consts; |
190 val {constants, constraints} = Consts.dest consts; |
190 val extern_const = Name_Space.extern ctxt (#1 constants); |
191 val extern_const = Name_Space.extern ctxt (#1 constants); |
191 val {classes, default, types, ...} = Type.rep_tsig tsig; |
192 val {classes, default, types, ...} = Type.rep_tsig tsig; |
192 val (class_space, class_algebra) = classes; |
193 val (class_space, class_algebra) = classes; |
193 val classes = Sorts.classes_of class_algebra; |
194 val classes = Sorts.classes_of class_algebra; |