1.1 --- a/src/Pure/Isar/isar_output.ML	Mon Nov 13 20:08:52 2006 +0100
     1.2 +++ b/src/Pure/Isar/isar_output.ML	Mon Nov 13 20:10:02 2006 +0100
     1.3 @@ -462,6 +462,8 @@
     1.4  fun pretty_prf full ctxt thms =
     1.5    Pretty.chunks (map (ProofContext.pretty_proof_of ctxt full) thms);
     1.6  
     1.7 +fun pretty_theory name = (ThyInfo.theory name; Pretty.str name);
     1.8 +
     1.9  
    1.10  (* Isar output *)
    1.11  
    1.12 @@ -520,7 +522,7 @@
    1.13    ("subgoals", output_goals false),
    1.14    ("prf", args Attrib.thms (output (pretty_prf false))),
    1.15    ("full_prf", args Attrib.thms (output (pretty_prf true))),
    1.16 -  ("theory", args (Scan.lift Args.name) ((K o K o tap) use_thy)),
    1.17 +  ("theory", args (Scan.lift Args.name) (output (K pretty_theory))),
    1.18    ("ML", args (Scan.lift Args.name) (output_ml ml_val)),
    1.19    ("ML_type", args (Scan.lift Args.name) (output_ml ml_type)),
    1.20    ("ML_struct", args (Scan.lift Args.name) (output_ml ml_struct))];