# HG changeset patch
# User haftmann
# Date 1414068228 -7200
# Node ID 1df01f0c05895c80bb8af58630c3f71184383eb3
# Parent  0997ea62e868f9b2d84a53381928efa6b102c357
tuned language and spelling

diff -r 0997ea62e868 -r 1df01f0c0589 src/HOL/Import/import_data.ML
--- a/src/HOL/Import/import_data.ML	Thu Oct 23 14:04:05 2014 +0200
+++ b/src/HOL/Import/import_data.ML	Thu Oct 23 14:43:48 2014 +0200
@@ -114,7 +114,7 @@
     (Scan.lift (Parse.name -- Parse.name -- Parse.name) >>
       (fn ((tyname, absname), repname) => Thm.declaration_attribute
         (fn th => Context.mapping (add_typ_def tyname absname repname th) I)))
-  "declare a type_definion theorem as a map for an imported type abs rep")
+  "declare a type_definition theorem as a map for an imported type with abs and rep")
 
 val _ =
   Outer_Syntax.command @{command_spec "import_type_map"}