src/HOL/BNF/Tools/bnf_wrap.ML
changeset 50214 67fb9a168d10
parent 49692 a8a3b82b37f8
child 51380 cac8c9a636b6
--- a/src/HOL/BNF/Tools/bnf_wrap.ML	Mon Nov 26 13:54:43 2012 +0100
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Mon Nov 26 14:43:28 2012 +0100
@@ -675,7 +675,7 @@
     >> (pairself (exists I) o split_list)) (false, false);
 
 val _ =
-  Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wraps an existing datatype"
+  Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wrap an existing datatype"
     ((parse_wrap_options -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) --
       Parse.term -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss --
         Scan.optional parse_bound_termss []) ([], [])) ([], ([], [])))