doc-src/antiquote_setup.ML
changeset 24920 2a45e400fdad
parent 24584 01e83ffa6c54
child 26385 ae7564661e76
     1.1 --- a/doc-src/antiquote_setup.ML	Mon Oct 08 22:06:32 2007 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Tue Oct 09 00:20:13 2007 +0200
     1.3 @@ -76,7 +76,7 @@
     1.4      #> space_implode "\\par\\smallskip%\n"
     1.5      #> enclose "\\isa{" "}");
     1.6  
     1.7 -fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.revert_skolems ctxt;
     1.8 +fun pretty_term ctxt = Syntax.pretty_term ctxt o ProofContext.revert_skolems ctxt;
     1.9  fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
    1.10  
    1.11  in