misc tuning and simplification;
authorwenzelm
Thu Apr 15 20:37:27 2010 +0200 (2010-04-15)
changeset 361572fb3e278a5d7
parent 36156 6f0a8f6b1671
child 36158 d2ad76e374d3
misc tuning and simplification;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Thu Apr 15 20:31:21 2010 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Apr 15 20:37:27 2010 +0200
     1.3 @@ -346,15 +346,12 @@
     1.4  
     1.5  (* add type constructors *)
     1.6  
     1.7 -val type_syntax = Syntax.mark_type oo full_name;
     1.8 +fun type_syntax thy (b, n, mx) = (Syntax.mark_type (full_name thy b), Syntax.make_type n, mx);
     1.9  
    1.10  fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
    1.11    let
    1.12 -    val syn' =
    1.13 -      Syntax.update_type_gram true Syntax.mode_default
    1.14 -        (map (fn (a, n, mx) => (type_syntax thy a, Syntax.make_type n, mx)) types) syn;
    1.15 -    val decls = map (fn (a, n, _) => (a, n)) types;
    1.16 -    val tsig' = fold (Type.add_type naming) decls tsig;
    1.17 +    val syn' = Syntax.update_type_gram true Syntax.mode_default (map (type_syntax thy) types) syn;
    1.18 +    val tsig' = fold (fn (a, n, _) => Type.add_type naming (a, n)) types tsig;
    1.19    in (naming, syn', tsig', consts) end);
    1.20  
    1.21  
    1.22 @@ -373,9 +370,8 @@
    1.23      let
    1.24        val ctxt = ProofContext.init thy;
    1.25        val syn' =
    1.26 -        Syntax.update_type_gram true Syntax.mode_default
    1.27 -          [(type_syntax thy b, Syntax.make_type (length vs), mx)] syn;
    1.28 -      val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
    1.29 +        Syntax.update_type_gram true Syntax.mode_default [type_syntax thy (b, length vs, mx)] syn;
    1.30 +      val abbr = (b, vs, parse_typ ctxt rhs)
    1.31          handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
    1.32        val tsig' = Type.add_abbrev naming abbr tsig;
    1.33      in (naming, syn', tsig', consts) end);