--- 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! *)