doc-src/antiquote_setup.ML
changeset 26710 f79aa228c582
parent 26461 da989545e59c
child 26742 5a86bc79431c
     1.1 --- a/doc-src/antiquote_setup.ML	Thu Apr 17 16:30:55 2008 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Thu Apr 17 22:22:19 2008 +0200
     1.3 @@ -83,7 +83,7 @@
     1.4      #> space_implode "\\par\\smallskip%\n"
     1.5      #> enclose "\\isa{" "}");
     1.6  
     1.7 -fun pretty_term ctxt = Syntax.pretty_term ctxt o ProofContext.revert_skolems ctxt;
     1.8 +fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
     1.9  fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
    1.10  
    1.11  in