changeset 46923 | 947f63062022 |
parent 46916 | e7ea35b41e2d |
child 47061 | 355317493f34 |
--- a/src/Pure/Isar/overloading.ML Wed Mar 14 17:52:38 2012 +0100 +++ b/src/Pure/Isar/overloading.ML Wed Mar 14 18:09:05 2012 +0100 @@ -174,7 +174,7 @@ Pretty.block (Pretty.breaks [Pretty.str v, Pretty.str "==", Pretty.str (Proof_Context.extern_const lthy c), Pretty.str "::", Syntax.pretty_typ lthy ty]); - in Pretty.str "overloading" :: map pr_operation overloading end; + in Pretty.command "overloading" :: map pr_operation overloading end; fun conclude lthy = let