'note': Toplevel.print;
authorwenzelm
Tue Jun 01 18:12:45 1999 +0200 (1999-06-01 ago)
changeset 67559f830d69a46d
parent 6754 c23c542a32e5
child 6756 fe6eb161df3e
'note': Toplevel.print;
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Jun 01 18:01:01 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Jun 01 18:12:45 1999 +0200
     1.3 @@ -282,7 +282,7 @@
     1.4  
     1.5  val factsP =
     1.6    OuterSyntax.command "note" "define facts" K.prf_decl
     1.7 -    (facts -- P.marg_comment >> (Toplevel.proof o IsarThy.have_facts));
     1.8 +    (facts -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.have_facts)));
     1.9  
    1.10  
    1.11  (* proof context *)