src/Pure/sign.ML
changeset 36179 f45c708bcc01
parent 36157 2fb3e278a5d7
child 36449 78721f3adb13
     1.1 --- a/src/Pure/sign.ML	Fri Apr 16 22:18:59 2010 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri Apr 16 22:45:07 2010 +0200
     1.3 @@ -72,8 +72,7 @@
     1.4    val add_defsort_i: sort -> theory -> theory
     1.5    val add_types: (binding * int * mixfix) list -> theory -> theory
     1.6    val add_nonterminals: binding list -> theory -> theory
     1.7 -  val add_tyabbrs: (binding * string list * string * mixfix) list -> theory -> theory
     1.8 -  val add_tyabbrs_i: (binding * string list * typ * mixfix) list -> theory -> theory
     1.9 +  val add_type_abbrev: binding * string list * typ -> theory -> theory
    1.10    val add_syntax: (string * string * mixfix) list -> theory -> theory
    1.11    val add_syntax_i: (string * typ * mixfix) list -> theory -> theory
    1.12    val add_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
    1.13 @@ -346,38 +345,25 @@
    1.14  
    1.15  (* add type constructors *)
    1.16  
    1.17 -fun type_syntax thy (b, n, mx) = (Syntax.mark_type (full_name thy b), Syntax.make_type n, mx);
    1.18 -
    1.19  fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
    1.20    let
    1.21 -    val syn' = Syntax.update_type_gram true Syntax.mode_default (map (type_syntax thy) types) syn;
    1.22 +    fun type_syntax (b, n, mx) =
    1.23 +      (Syntax.mark_type (Name_Space.full_name naming b), Syntax.make_type n, mx);
    1.24 +    val syn' = Syntax.update_type_gram true Syntax.mode_default (map type_syntax types) syn;
    1.25      val tsig' = fold (fn (a, n, _) => Type.add_type naming (a, n)) types tsig;
    1.26    in (naming, syn', tsig', consts) end);
    1.27  
    1.28  
    1.29  (* add nonterminals *)
    1.30  
    1.31 -fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
    1.32 -  let
    1.33 -    val tsig' = fold (Type.add_nonterminal naming) ns tsig;
    1.34 -  in (naming, syn, tsig', consts) end);
    1.35 +fun add_nonterminals ns = map_sign (fn (naming, syn, tsig, consts) =>
    1.36 +  (naming, syn, fold (Type.add_nonterminal naming) ns tsig, consts));
    1.37  
    1.38  
    1.39  (* add type abbreviations *)
    1.40  
    1.41 -fun gen_add_tyabbr parse_typ (b, vs, rhs, mx) thy =
    1.42 -  thy |> map_sign (fn (naming, syn, tsig, consts) =>
    1.43 -    let
    1.44 -      val ctxt = ProofContext.init thy;
    1.45 -      val syn' =
    1.46 -        Syntax.update_type_gram true Syntax.mode_default [type_syntax thy (b, length vs, mx)] syn;
    1.47 -      val abbr = (b, vs, parse_typ ctxt rhs)
    1.48 -        handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
    1.49 -      val tsig' = Type.add_abbrev naming abbr tsig;
    1.50 -    in (naming, syn', tsig', consts) end);
    1.51 -
    1.52 -val add_tyabbrs = fold (gen_add_tyabbr Syntax.parse_typ);
    1.53 -val add_tyabbrs_i = fold (gen_add_tyabbr (K I));
    1.54 +fun add_type_abbrev abbr = map_sign (fn (naming, syn, tsig, consts) =>
    1.55 +  (naming, syn, Type.add_abbrev naming abbr tsig, consts));
    1.56  
    1.57  
    1.58  (* modify syntax *)