src/HOL/Import/import_syntax.ML
changeset 27353 71c4dd53d4cb
parent 24867 e5b55d7be9bb
child 27775 a9d16f8b997a
     1.1 --- a/src/HOL/Import/import_syntax.ML	Wed Jun 25 14:54:45 2008 +0200
     1.2 +++ b/src/HOL/Import/import_syntax.ML	Wed Jun 25 17:38:32 2008 +0200
     1.3 @@ -223,7 +223,7 @@
     1.4  val append_dump = (P.verbatim || P.string) >> add_dump
     1.5  
     1.6  fun setup () =
     1.7 -  (OuterSyntax.keywords[">"];
     1.8 +  (OuterKeyword.keyword ">";
     1.9     OuterSyntax.command "import_segment"
    1.10  		       "Set import segment name"
    1.11  		       K.thy_decl (import_segment >> Toplevel.theory);