1.1 --- a/src/HOL/Tools/typedef_package.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -273,7 +273,9 @@
     1.4  
     1.5  local structure P = OuterParse and K = OuterKeyword in
     1.6  
     1.7 -val typedeclP =
     1.8 +val _ = OuterSyntax.keywords ["morphisms"];
     1.9 +
    1.10 +val _ =
    1.11    OuterSyntax.command "typedecl" "type declaration (HOL)" K.thy_decl
    1.12      (P.type_args -- P.name -- P.opt_infix >> (fn ((vs, t), mx) =>
    1.13        Toplevel.theory (add_typedecls [(t, vs, mx)])));
    1.14 @@ -289,14 +291,10 @@
    1.15  fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
    1.16    typedef ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
    1.17  
    1.18 -val typedefP =
    1.19 +val _ =
    1.20    OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal
    1.21      (typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef)));
    1.22  
    1.23 -
    1.24 -val _ = OuterSyntax.add_keywords ["morphisms"];
    1.25 -val _ = OuterSyntax.add_parsers [typedeclP, typedefP];
    1.26 -
    1.27  end;
    1.28  
    1.29  end;