# HG changeset patch
# User wenzelm
# Date 1271356647 -7200
# Node ID 2fb3e278a5d7282d78d13eed881a62c564d76978
# Parent  6f0a8f6b1671ef83a41236a9db8085e6dc2ccb35
misc tuning and simplification;

diff -r 6f0a8f6b1671 -r 2fb3e278a5d7 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Apr 15 20:31:21 2010 +0200
+++ b/src/Pure/sign.ML	Thu Apr 15 20:37:27 2010 +0200
@@ -346,15 +346,12 @@
 
 (* add type constructors *)
 
-val type_syntax = Syntax.mark_type oo full_name;
+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 (fn (a, n, mx) => (type_syntax thy a, Syntax.make_type n, mx)) types) syn;
-    val decls = map (fn (a, n, _) => (a, n)) types;
-    val tsig' = fold (Type.add_type naming) decls tsig;
+    val syn' = Syntax.update_type_gram true Syntax.mode_default (map (type_syntax thy) types) syn;
+    val tsig' = fold (fn (a, n, _) => Type.add_type naming (a, n)) types tsig;
   in (naming, syn', tsig', consts) end);
 
 
@@ -373,9 +370,8 @@
     let
       val ctxt = ProofContext.init thy;
       val syn' =
-        Syntax.update_type_gram true Syntax.mode_default
-          [(type_syntax thy b, Syntax.make_type (length vs), mx)] syn;
-      val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
+        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);