changeset 6755 | 9f830d69a46d |
parent 6742 | 6b5cb872d997 |
child 6757 | 604d1445c9f3 |
--- 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 *)