--- a/src/Pure/Isar/method.ML Fri Nov 30 21:47:44 2012 +0100
+++ b/src/Pure/Isar/method.ML Fri Nov 30 22:38:06 2012 +0100
@@ -316,9 +316,10 @@
let
val ctxt = Proof_Context.init_global thy;
val meths = Methods.get thy;
- fun prt_meth (name, (_, "")) = Pretty.str name
+ fun prt_meth (name, (_, "")) = Pretty.mark_str name
| prt_meth (name, (_, comment)) =
- Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
+ Pretty.block
+ (Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
in
[Pretty.big_list "methods:" (map prt_meth (Name_Space.extern_table ctxt meths))]
|> Pretty.chunks |> Pretty.writeln