# HG changeset patch
# User berghofe
# Date 1002731901 -7200
# Node ID 064833efb4797d8f747b80e57b14ccb91768f4f9
# Parent  592923615f77328878e419b61b6d9d51ddaf5b59
Exported output_with.

diff -r 592923615f77 -r 064833efb479 src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Wed Oct 10 18:37:52 2001 +0200
+++ b/src/Pure/Isar/isar_output.ML	Wed Oct 10 18:38:21 2001 +0200
@@ -25,6 +25,8 @@
   val quotes: bool ref
   val indent: int ref
   val source: bool ref
+  val output_with: (Proof.context -> 'a -> Pretty.T) -> Args.src ->
+    Proof.context -> 'a -> string
 end;
 
 structure IsarOutput: ISAR_OUTPUT =
@@ -269,8 +271,6 @@
 
 (* commands *)
 
-local
-
 fun cond_quote prt =
   if ! quotes then Pretty.quote prt else prt;
 
@@ -312,8 +312,6 @@
   Pretty.chunks (Proof.pretty_goals main_goal (Toplevel.proof_of state
       handle Toplevel.UNDEF => error "No proof state")))) src state;
 
-in
-
 val _ = add_commands
  [("text", args (Scan.lift Args.name) (output_with (K pretty_text))),
   ("thm", args Attrib.local_thmss (output_with pretty_thm)),
@@ -326,5 +324,3 @@
   ("subgoals", output_goals false)];
 
 end;
-
-end;