1.1 --- a/src/HOL/Library/simps_case_conv.ML	Wed Jul 23 23:08:22 2014 +0200
     1.2 +++ b/src/HOL/Library/simps_case_conv.ML	Wed Jul 23 23:16:44 2014 +0200
     1.3 @@ -220,7 +220,7 @@
     1.4  
     1.5  val _ =
     1.6    Outer_Syntax.local_theory @{command_spec "case_of_simps"}
     1.7 -    "turns a list of equations into a case expression"
     1.8 +    "turn a list of equations into a case expression"
     1.9      (Parse_Spec.opt_thm_name ":"  -- Parse_Spec.xthms1 >> case_of_simps_cmd)
    1.10  
    1.11  val parse_splits = @{keyword "("} |-- Parse.reserved "splits" |-- @{keyword ":"} |--