# HG changeset patch
# User haftmann
# Date 1163428995 -3600
# Node ID d89d2cb8a05fc710df29e25145076ae39b061335
# Parent  b5c7efb57b3ed28bee51fd2af8c4930a6dde5350
added theory antiquotation

diff -r b5c7efb57b3e -r d89d2cb8a05f src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Mon Nov 13 15:43:14 2006 +0100
+++ b/src/Pure/Isar/isar_output.ML	Mon Nov 13 15:43:15 2006 +0100
@@ -232,8 +232,8 @@
 fun err_bad_nesting pos =
   error ("Bad nesting of commands in presentation" ^ pos);
 
-fun edge1 f (x, y) = the_default I (Option.map (Buffer.add o f) (if x = y then NONE else x));
-fun edge2 f (x, y) = the_default I (Option.map (Buffer.add o f) (if x = y then NONE else y));
+fun edge1 f (x : string option, y) = the_default I (Option.map (Buffer.add o f) (if x = y then NONE else x));
+fun edge2 f (x : string option, y) = the_default I (Option.map (Buffer.add o f) (if x = y then NONE else y));
 
 val begin_tag = edge2 Latex.begin_tag;
 val end_tag = edge1 Latex.end_tag;
@@ -520,6 +520,7 @@
   ("subgoals", output_goals false),
   ("prf", args Attrib.thms (output (pretty_prf false))),
   ("full_prf", args Attrib.thms (output (pretty_prf true))),
+  ("theory", args (Scan.lift Args.name) ((K o K o tap) use_thy)),
   ("ML", args (Scan.lift Args.name) (output_ml ml_val)),
   ("ML_type", args (Scan.lift Args.name) (output_ml ml_type)),
   ("ML_struct", args (Scan.lift Args.name) (output_ml ml_struct))];