# HG changeset patch
# User wenzelm
# Date 928253565 -7200
# Node ID 9f830d69a46d0bb5f8747bcd12d09d6eb28bf0af
# Parent  c23c542a32e5030e2d5f50fb37fa779022762eee
'note': Toplevel.print;

diff -r c23c542a32e5 -r 9f830d69a46d src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Jun 01 18:01:01 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jun 01 18:12:45 1999 +0200
@@ -282,7 +282,7 @@
 
 val factsP =
   OuterSyntax.command "note" "define facts" K.prf_decl
-    (facts -- P.marg_comment >> (Toplevel.proof o IsarThy.have_facts));
+    (facts -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.have_facts)));
 
 
 (* proof context *)