src/Pure/sign.ML
changeset 33173 b8ca12f6681a
parent 33172 61ee96bc9895
child 33385 fb2358edcfb6
     1.1 --- a/src/Pure/sign.ML	Sun Oct 25 20:54:21 2009 +0100
     1.2 +++ b/src/Pure/sign.ML	Sun Oct 25 21:35:46 2009 +0100
     1.3 @@ -90,10 +90,10 @@
     1.4    val del_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
     1.5    val del_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
     1.6    val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
     1.7 -  val declare_const: Properties.T -> (binding * typ) * mixfix -> theory -> term * theory
     1.8 +  val declare_const: (binding * typ) * mixfix -> theory -> term * theory
     1.9    val add_consts: (binding * string * mixfix) list -> theory -> theory
    1.10    val add_consts_i: (binding * typ * mixfix) list -> theory -> theory
    1.11 -  val add_abbrev: string -> Properties.T -> binding * term -> theory -> (term * term) * theory
    1.12 +  val add_abbrev: string -> binding * term -> theory -> (term * term) * theory
    1.13    val revert_abbrev: string -> string -> theory -> theory
    1.14    val add_const_constraint: string * typ option -> theory -> theory
    1.15    val primitive_class: binding * class list -> theory -> theory
    1.16 @@ -434,7 +434,7 @@
    1.17    let
    1.18      val syn' = Syntax.update_type_gram (map (fn (a, n, mx) => (Name.of_binding a, n, mx)) types) syn;
    1.19      val decls = map (fn (a, n, mx) => (Binding.map_name (Syntax.type_name mx) a, n)) types;
    1.20 -    val tsig' = fold (Type.add_type naming []) decls tsig;
    1.21 +    val tsig' = fold (Type.add_type naming) decls tsig;
    1.22    in (naming, syn', tsig', consts) end);
    1.23  
    1.24  
    1.25 @@ -443,7 +443,7 @@
    1.26  fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
    1.27    let
    1.28      val syn' = Syntax.update_consts (map Name.of_binding ns) syn;
    1.29 -    val tsig' = fold (Type.add_nonterminal naming []) ns tsig;
    1.30 +    val tsig' = fold (Type.add_nonterminal naming) ns tsig;
    1.31    in (naming, syn', tsig', consts) end);
    1.32  
    1.33  
    1.34 @@ -457,7 +457,7 @@
    1.35        val b = Binding.map_name (Syntax.type_name mx) a;
    1.36        val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
    1.37          handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
    1.38 -      val tsig' = Type.add_abbrev naming [] abbr tsig;
    1.39 +      val tsig' = Type.add_abbrev naming abbr tsig;
    1.40      in (naming, syn', tsig', consts) end);
    1.41  
    1.42  val add_tyabbrs = fold (gen_add_tyabbr Syntax.parse_typ);
    1.43 @@ -495,7 +495,7 @@
    1.44  
    1.45  local
    1.46  
    1.47 -fun gen_add_consts parse_typ authentic tags raw_args thy =
    1.48 +fun gen_add_consts parse_typ authentic raw_args thy =
    1.49    let
    1.50      val ctxt = ProofContext.init thy;
    1.51      val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
    1.52 @@ -512,20 +512,20 @@
    1.53      val args = map prep raw_args;
    1.54    in
    1.55      thy
    1.56 -    |> map_consts (fold (Consts.declare authentic (naming_of thy) tags o #1) args)
    1.57 +    |> map_consts (fold (Consts.declare authentic (naming_of thy) o #1) args)
    1.58      |> add_syntax_i (map #2 args)
    1.59      |> pair (map #3 args)
    1.60    end;
    1.61  
    1.62  in
    1.63  
    1.64 -fun add_consts args = snd o gen_add_consts Syntax.parse_typ false [] args;
    1.65 -fun add_consts_i args = snd o gen_add_consts (K I) false [] args;
    1.66 +fun add_consts args = snd o gen_add_consts Syntax.parse_typ false args;
    1.67 +fun add_consts_i args = snd o gen_add_consts (K I) false args;
    1.68  
    1.69 -fun declare_const tags ((b, T), mx) thy =
    1.70 +fun declare_const ((b, T), mx) thy =
    1.71    let
    1.72      val pos = Binding.pos_of b;
    1.73 -    val ([const as Const (c, _)], thy') = gen_add_consts (K I) true tags [(b, T, mx)] thy;
    1.74 +    val ([const as Const (c, _)], thy') = gen_add_consts (K I) true [(b, T, mx)] thy;
    1.75      val _ = Position.report (Markup.const_decl c) pos;
    1.76    in (const, thy') end;
    1.77  
    1.78 @@ -534,14 +534,14 @@
    1.79  
    1.80  (* abbreviations *)
    1.81  
    1.82 -fun add_abbrev mode tags (b, raw_t) thy =
    1.83 +fun add_abbrev mode (b, raw_t) thy =
    1.84    let
    1.85      val pp = Syntax.pp_global thy;
    1.86      val prep_tm = no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
    1.87      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
    1.88        handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
    1.89      val (res, consts') = consts_of thy
    1.90 -      |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (b, t);
    1.91 +      |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode (b, t);
    1.92    in (res, thy |> map_consts (K consts')) end;
    1.93  
    1.94  fun revert_abbrev mode c = map_consts (Consts.revert_abbrev mode c);