equal
deleted
inserted
replaced
32 ); |
32 ); |
33 |
33 |
34 fun print_structures ctxt = |
34 fun print_structures ctxt = |
35 let |
35 let |
36 val structs = Data.get (Context.Proof ctxt); |
36 val structs = Data.get (Context.Proof ctxt); |
37 val pretty_term = Pretty.quote o ProofContext.pretty_term ctxt; |
37 val pretty_term = Pretty.quote o Syntax.pretty_term ctxt; |
38 fun pretty_struct ((s, ts), _) = Pretty.block |
38 fun pretty_struct ((s, ts), _) = Pretty.block |
39 [Pretty.str s, Pretty.str ":", Pretty.brk 1, |
39 [Pretty.str s, Pretty.str ":", Pretty.brk 1, |
40 Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))]; |
40 Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))]; |
41 in Pretty.writeln (Pretty.big_list "Algebraic structures:" (map pretty_struct structs)) end; |
41 in Pretty.writeln (Pretty.big_list "Algebraic structures:" (map pretty_struct structs)) end; |
42 |
42 |