# HG changeset patch
# User wenzelm
# Date 1271450707 -7200
# Node ID f45c708bcc01a9f5467b710b1704ee69cb4282dd
# Parent  0e5c133b48b663e3bc67d6182c0dbb39a2928bec
replaced old Sign.add_tyabbrs(_i) by Sign.add_type_abbrev (without mixfix);
misc tuning and simplification;

diff -r 0e5c133b48b6 -r f45c708bcc01 src/Pure/Isar/typedecl.ML
--- a/src/Pure/Isar/typedecl.ML	Fri Apr 16 22:18:59 2010 +0200
+++ b/src/Pure/Isar/typedecl.ML	Fri Apr 16 22:45:07 2010 +0200
@@ -89,7 +89,7 @@
       handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
   in
     lthy
-    |> basic_decl (fn _ => Sign.add_tyabbrs_i [(b, vs, rhs, NoSyn)]) (b, length vs, mx)
+    |> basic_decl (fn _ => Sign.add_type_abbrev (b, vs, rhs)) (b, length vs, mx)
     |> snd
     |> pair name
   end;
diff -r 0e5c133b48b6 -r f45c708bcc01 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Apr 16 22:18:59 2010 +0200
+++ b/src/Pure/sign.ML	Fri Apr 16 22:45:07 2010 +0200
@@ -72,8 +72,7 @@
   val add_defsort_i: sort -> theory -> theory
   val add_types: (binding * int * mixfix) list -> theory -> theory
   val add_nonterminals: binding list -> theory -> theory
-  val add_tyabbrs: (binding * string list * string * mixfix) list -> theory -> theory
-  val add_tyabbrs_i: (binding * string list * typ * mixfix) list -> theory -> theory
+  val add_type_abbrev: binding * string list * typ -> theory -> theory
   val add_syntax: (string * string * mixfix) list -> theory -> theory
   val add_syntax_i: (string * typ * mixfix) list -> theory -> theory
   val add_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
@@ -346,38 +345,25 @@
 
 (* add type constructors *)
 
-fun type_syntax thy (b, n, mx) = (Syntax.mark_type (full_name thy b), Syntax.make_type n, mx);
-
 fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
   let
-    val syn' = Syntax.update_type_gram true Syntax.mode_default (map (type_syntax thy) types) syn;
+    fun type_syntax (b, n, mx) =
+      (Syntax.mark_type (Name_Space.full_name naming b), Syntax.make_type n, mx);
+    val syn' = Syntax.update_type_gram true Syntax.mode_default (map type_syntax types) syn;
     val tsig' = fold (fn (a, n, _) => Type.add_type naming (a, n)) types tsig;
   in (naming, syn', tsig', consts) end);
 
 
 (* add nonterminals *)
 
-fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
-  let
-    val tsig' = fold (Type.add_nonterminal naming) ns tsig;
-  in (naming, syn, tsig', consts) end);
+fun add_nonterminals ns = map_sign (fn (naming, syn, tsig, consts) =>
+  (naming, syn, fold (Type.add_nonterminal naming) ns tsig, consts));
 
 
 (* add type abbreviations *)
 
-fun gen_add_tyabbr parse_typ (b, vs, rhs, mx) thy =
-  thy |> map_sign (fn (naming, syn, tsig, consts) =>
-    let
-      val ctxt = ProofContext.init thy;
-      val syn' =
-        Syntax.update_type_gram true Syntax.mode_default [type_syntax thy (b, length vs, mx)] syn;
-      val abbr = (b, vs, parse_typ ctxt rhs)
-        handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
-      val tsig' = Type.add_abbrev naming abbr tsig;
-    in (naming, syn', tsig', consts) end);
-
-val add_tyabbrs = fold (gen_add_tyabbr Syntax.parse_typ);
-val add_tyabbrs_i = fold (gen_add_tyabbr (K I));
+fun add_type_abbrev abbr = map_sign (fn (naming, syn, tsig, consts) =>
+  (naming, syn, Type.add_abbrev naming abbr tsig, consts));
 
 
 (* modify syntax *)