# HG changeset patch
# User wenzelm
# Date 1331744945 -3600
# Node ID 947f630620222df1f37e71c8cf10e5e87f12a7b9
# Parent  3717f3878714aec27b2257426c678ff01037b358
tuned messages;

diff -r 3717f3878714 -r 947f63062022 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Mar 14 17:52:38 2012 +0100
+++ b/src/Pure/Isar/class.ML	Wed Mar 14 18:09:05 2012 +0100
@@ -499,7 +499,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 "instantiation" :: map pr_arity tycos @ map pr_param params end;
+  in Pretty.command "instantiation" :: map pr_arity tycos @ map pr_param params end;
 
 fun conclude lthy =
   let
diff -r 3717f3878714 -r 947f63062022 src/Pure/Isar/overloading.ML
--- 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