diff -r 14c3dd5ee2ad -r 7b8c4fe235aa CookBook/Recipes/Antiquotes.thy
--- a/CookBook/Recipes/Antiquotes.thy	Wed Jan 14 21:46:04 2009 +0000
+++ b/CookBook/Recipes/Antiquotes.thy	Wed Jan 14 23:44:14 2009 +0000
@@ -4,8 +4,6 @@
 begin
 
 
-
-
 section {* Useful Document Antiquotations *}
 
 text {*
@@ -90,7 +88,7 @@
   hints what the result of the ML-code should be and to check the consistency of 
   the actual result with these hints. For this we are going to implement the 
   antiquotation  
-  @{text "@{ML_response \"expr\" \"pat\"}"}
+  @{text "@{ML_resp \"expr\" \"pat\"}"}
   whose first argument is the ML-code and the second is a pattern specifying
   the result. To add some convenience and allow dealing with large outputs,
   the user can give a partial specification including abbreviations 
@@ -117,41 +115,43 @@
 *}
 
 
-ML{*fun add_response_indicator pat =
+ML{*fun add_resp_indicator pat =
   map (fn s => "> " ^ s) (space_explode "\n" pat) *}
 
 text {* 
   The rest of the code of the antiquotation is
-  *}
+*}
 
-ML{*fun output_ml_response src ctxt ((code_txt,pat),pos) = 
+ML{*fun output_ml_resp src ctxt ((code_txt,pat),pos) = 
   (ML_Context.eval_in (SOME ctxt) false pos (ml_pat (code_txt,pat));
    let 
-     val output = (space_explode "\n" code_txt) @ (add_response_indicator pat)
+     val output = (space_explode "\n" code_txt) @ (add_resp_indicator pat)
    in 
      ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt output 
    end)
 
 val _ = ThyOutput.add_commands
- [("ML_response", 
+ [("ML_resp", 
      ThyOutput.args 
       (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
-        output_ml_response)]*}
+        output_ml_resp)]*}
 
 text {*
-  This extended antiquotation allows us to write 
-  @{text [display] "@{ML_response [display] \"true andalso false\" \"false\"}"}
+  This extended antiquotation allows us to write
+ 
+  @{text [display] "@{ML_resp [display] \"true andalso false\" \"false\"}"}
+
   to obtain
 
-@{ML_response [display] "true andalso false" "false"} 
+  @{ML_resp [display] "true andalso false" "false"} 
 
   or 
 
-@{text [display] "@{ML_response [display] \"let val i = 3 in (i * i,\"foo\") end\" \"(9,\<dots>)\"}"}
+  @{text [display] "@{ML_resp [display] \"let val i = 3 in (i * i,\"foo\") end\" \"(9,\<dots>)\"}"}
   
   to obtain
 
-@{ML_response [display] "let val i = 3 in (i * i,\"foo\") end" "(9,\<dots>)"} 
+  @{ML_resp [display] "let val i = 3 in (i * i,\"foo\") end" "(9,\<dots>)"} 
 
   In both cases, the check by the compiler ensures that code and result match. A limitation
   of this antiquotation is that the hints can only be given for results that can actually