1.1 --- a/src/Pure/Isar/typedecl.ML	Fri Apr 16 22:18:59 2010 +0200
     1.2 +++ b/src/Pure/Isar/typedecl.ML	Fri Apr 16 22:45:07 2010 +0200
     1.3 @@ -89,7 +89,7 @@
     1.4        handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
     1.5    in
     1.6      lthy
     1.7 -    |> basic_decl (fn _ => Sign.add_tyabbrs_i [(b, vs, rhs, NoSyn)]) (b, length vs, mx)
     1.8 +    |> basic_decl (fn _ => Sign.add_type_abbrev (b, vs, rhs)) (b, length vs, mx)
     1.9      |> snd
    1.10      |> pair name
    1.11    end;

     2.1 --- a/src/Pure/sign.ML	Fri Apr 16 22:18:59 2010 +0200
     2.2 +++ b/src/Pure/sign.ML	Fri Apr 16 22:45:07 2010 +0200
     2.3 @@ -72,8 +72,7 @@
     2.4    val add_defsort_i: sort -> theory -> theory
     2.5    val add_types: (binding * int * mixfix) list -> theory -> theory
     2.6    val add_nonterminals: binding list -> theory -> theory
     2.7 -  val add_tyabbrs: (binding * string list * string * mixfix) list -> theory -> theory
     2.8 -  val add_tyabbrs_i: (binding * string list * typ * mixfix) list -> theory -> theory
     2.9 +  val add_type_abbrev: binding * string list * typ -> theory -> theory
    2.10    val add_syntax: (string * string * mixfix) list -> theory -> theory
    2.11    val add_syntax_i: (string * typ * mixfix) list -> theory -> theory
    2.12    val add_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
    2.13 @@ -346,38 +345,25 @@
    2.14  
    2.15  (* add type constructors *)
    2.16  
    2.17 -fun type_syntax thy (b, n, mx) = (Syntax.mark_type (full_name thy b), Syntax.make_type n, mx);
    2.18 -
    2.19  fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
    2.20    let
    2.21 -    val syn' = Syntax.update_type_gram true Syntax.mode_default (map (type_syntax thy) types) syn;
    2.22 +    fun type_syntax (b, n, mx) =
    2.23 +      (Syntax.mark_type (Name_Space.full_name naming b), Syntax.make_type n, mx);
    2.24 +    val syn' = Syntax.update_type_gram true Syntax.mode_default (map type_syntax types) syn;
    2.25      val tsig' = fold (fn (a, n, _) => Type.add_type naming (a, n)) types tsig;
    2.26    in (naming, syn', tsig', consts) end);
    2.27  
    2.28  
    2.29  (* add nonterminals *)
    2.30  
    2.31 -fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
    2.32 -  let
    2.33 -    val tsig' = fold (Type.add_nonterminal naming) ns tsig;
    2.34 -  in (naming, syn, tsig', consts) end);
    2.35 +fun add_nonterminals ns = map_sign (fn (naming, syn, tsig, consts) =>
    2.36 +  (naming, syn, fold (Type.add_nonterminal naming) ns tsig, consts));
    2.37  
    2.38  
    2.39  (* add type abbreviations *)
    2.40  
    2.41 -fun gen_add_tyabbr parse_typ (b, vs, rhs, mx) thy =
    2.42 -  thy |> map_sign (fn (naming, syn, tsig, consts) =>
    2.43 -    let
    2.44 -      val ctxt = ProofContext.init thy;
    2.45 -      val syn' =
    2.46 -        Syntax.update_type_gram true Syntax.mode_default [type_syntax thy (b, length vs, mx)] syn;
    2.47 -      val abbr = (b, vs, parse_typ ctxt rhs)
    2.48 -        handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
    2.49 -      val tsig' = Type.add_abbrev naming abbr tsig;
    2.50 -    in (naming, syn', tsig', consts) end);
    2.51 -
    2.52 -val add_tyabbrs = fold (gen_add_tyabbr Syntax.parse_typ);
    2.53 -val add_tyabbrs_i = fold (gen_add_tyabbr (K I));
    2.54 +fun add_type_abbrev abbr = map_sign (fn (naming, syn, tsig, consts) =>
    2.55 +  (naming, syn, Type.add_abbrev naming abbr tsig, consts));
    2.56  
    2.57  
    2.58  (* modify syntax *)