diff -r 7c9cb219b340 -r a18e60f597b6 src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Mon Nov 13 20:08:52 2006 +0100
+++ b/src/Pure/Isar/isar_output.ML	Mon Nov 13 20:10:02 2006 +0100
@@ -462,6 +462,8 @@
 fun pretty_prf full ctxt thms =
   Pretty.chunks (map (ProofContext.pretty_proof_of ctxt full) thms);
 
+fun pretty_theory name = (ThyInfo.theory name; Pretty.str name);
+
 
 (* Isar output *)
 
@@ -520,7 +522,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)),
+  ("theory", args (Scan.lift Args.name) (output (K pretty_theory))),
   ("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))];