# HG changeset patch
# User wenzelm
# Date 1191952134 -7200
# Node ID a220317465b495cf55e0630f7c5944ab92ec0f78
# Parent  34052359891452d8ceaaaf694a1d9dde2881c2e7
class: print result is for locale;

diff -r 340523598914 -r a220317465b4 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Oct 09 18:14:00 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Oct 09 19:48:54 2007 +0200
@@ -430,9 +430,9 @@
      Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") [] --  (* FIXME ?? *)
      Scan.optional (P.$$$ "(" |-- (P.$$$ "local_syntax" >> K true) --| P.$$$ ")") false --  (* FIXME ?? *)
      (P.$$$ "=" |-- class_val) -- P.opt_begin
-    >> (fn ((((bname, add_consts), local_syntax), (supclasses, elems)), begin) =>
-        Toplevel.begin_local_theory begin
-          (Class.class_cmd false bname supclasses elems add_consts #-> TheoryTarget.begin)));
+    >> (fn ((((name, add_consts), local_syntax), (supclasses, elems)), begin) =>
+        (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
+          (Class.class_cmd false name supclasses elems add_consts #-> TheoryTarget.begin)));
 
 val _ =
   OuterSyntax.command "subclass" "prove a subclass relation" K.thy_goal