src/Pure/Thy/document_antiquotations.ML
changeset 61704 3a010273df63
parent 61660 78b371644654
child 61705 546e6494049f
--- 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 *)