equal
deleted
inserted
replaced
131 |
131 |
132 fun hackish_string_of_term ctxt = |
132 fun hackish_string_of_term ctxt = |
133 (* FIXME: map_aterms (fn Free (s, T) => Free (if Name.is_internal s then "_" else s, T) | t => t) |
133 (* FIXME: map_aterms (fn Free (s, T) => Free (if Name.is_internal s then "_" else s, T) | t => t) |
134 #> *) Syntax.pretty_term ctxt |
134 #> *) Syntax.pretty_term ctxt |
135 #> Pretty.pure_string_of |
135 #> Pretty.pure_string_of |
136 #> Protocol_Message.clean_output |
|
137 #> simplify_spaces |
136 #> simplify_spaces |
138 |
137 |
139 val spying_version = "d" |
138 val spying_version = "d" |
140 |
139 |
141 fun spying false _ = () |
140 fun spying false _ = () |