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