tuned;
authorwenzelm
Thu, 19 Nov 2015 20:55:40 +0100
changeset 61704 3a010273df63
parent 61703 1f1354ca7ea7
child 61705 546e6494049f
tuned;
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 *)