# HG changeset patch
# User wenzelm
# Date 1447962940 -3600
# Node ID 3a010273df639e47105928b418f635d3fd33a0bf
# Parent  1f1354ca7ea727e2c2c6c37facac1d35aa69f663
tuned;

diff -r 1f1354ca7ea7 -r 3a010273df63 src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Thu Nov 19 18:43:41 2015 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Thu Nov 19 20:55:40 2015 +0100
@@ -11,10 +11,10 @@
 
 val _ =
   Theory.setup
-   (Thy_Output.antiquotation @{binding noindent} (Scan.succeed ()) (fn _ => fn () => "\\noindent") #>
-    Thy_Output.antiquotation @{binding smallskip} (Scan.succeed ()) (fn _ => fn () => "\\smallskip") #>
-    Thy_Output.antiquotation @{binding medskip} (Scan.succeed ()) (fn _ => fn () => "\\medskip") #>
-    Thy_Output.antiquotation @{binding bigskip} (Scan.succeed ()) (fn _ => fn () => "\\bigskip"));
+   (Thy_Output.antiquotation @{binding noindent} (Scan.succeed ()) (K (K "\\noindent")) #>
+    Thy_Output.antiquotation @{binding smallskip} (Scan.succeed ()) (K (K "\\smallskip")) #>
+    Thy_Output.antiquotation @{binding medskip} (Scan.succeed ()) (K (K "\\medskip")) #>
+    Thy_Output.antiquotation @{binding bigskip} (Scan.succeed ()) (K (K "\\bigskip")));
 
 
 (* control style *)