1.1 --- a/src/HOL/Import/import.ML	Thu Mar 15 17:45:54 2012 +0100
     1.2 +++ b/src/HOL/Import/import.ML	Thu Mar 15 19:02:34 2012 +0100
     1.3 @@ -238,8 +238,7 @@
     1.4  val append_dump = (Parse.verbatim || Parse.string) >> add_dump
     1.5  
     1.6  val _ =
     1.7 -  (Keyword.keyword ">";
     1.8 -   Outer_Syntax.command "import_segment"
     1.9 +  (Outer_Syntax.command "import_segment"
    1.10                         "Set import segment name"
    1.11                         Keyword.thy_decl (import_segment >> Toplevel.theory);
    1.12     Outer_Syntax.command "import_theory"