Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
antiquotation theory: plain Theory.requires, no peeking at ThyInfo;
authorwenzelm
Tue, 14 Nov 2006 15:29:54 +0100
changeset 21360 c63755004033
parent 21359 072e83a0b5bb
child 21361 653d1631f997
antiquotation theory: plain Theory.requires, no peeking at ThyInfo;
src/Pure/Isar/isar_output.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/isar_output.ML	Tue Nov 14 15:29:52 2006 +0100
+++ b/src/Pure/Isar/isar_output.ML	Tue Nov 14 15:29:54 2006 +0100
@@ -462,7 +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);
+fun pretty_theory ctxt name =
+  (Theory.requires (ProofContext.theory_of ctxt) name "presentation"; Pretty.str name);
 
 
 (* Isar output *)
@@ -522,7 +523,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) (output (K pretty_theory))),
+  ("theory", args (Scan.lift Args.name) (output 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))];
isabelle