equal
deleted
inserted
replaced
80 structure Code_Printer : CODE_PRINTER = |
80 structure Code_Printer : CODE_PRINTER = |
81 struct |
81 struct |
82 |
82 |
83 open Code_Thingol; |
83 open Code_Thingol; |
84 |
84 |
85 fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm thm); |
85 fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm); |
86 |
86 |
87 (** assembling text pieces **) |
87 (** assembling text pieces **) |
88 |
88 |
89 infixr 5 @@; |
89 infixr 5 @@; |
90 infixr 5 @|; |
90 infixr 5 @|; |