# HG changeset patch
# User wenzelm
# Date 1215716030 -7200
# Node ID 85bbd045ac3e9bf4849da449d14c77a15a66675e
# Parent  f3d92b5dcd45cec7987037b85a40dd5233102bc5
added print;

diff -r f3d92b5dcd45 -r 85bbd045ac3e src/Pure/Isar/isar.ML
--- a/src/Pure/Isar/isar.ML	Thu Jul 10 20:03:30 2008 +0200
+++ b/src/Pure/Isar/isar.ML	Thu Jul 10 20:53:50 2008 +0200
@@ -12,6 +12,7 @@
   val exn: unit -> (exn * string) option
   val context: unit -> Proof.context
   val goal: unit -> thm
+  val print: unit -> unit
   val >> : Toplevel.transition -> bool
   val >>> : Toplevel.transition list -> unit
   val linear_undo: int -> unit
@@ -162,6 +163,8 @@
   #2 (#2 (Proof.get_goal (Toplevel.proof_of (state ()))))
     handle Toplevel.UNDEF => error "No goal present";
 
+fun print () = Toplevel.print_state false (state ());
+
 
 (* interactive state transformations --- NOT THREAD-SAFE! *)