# HG changeset patch # User wenzelm # Date 1192111523 -7200 # Node ID 119793c846479e3fa9065076f0bc91e3249e84c0 # Parent ff15f76741bd6bad0b7ab7ced28c2932cd207dea replaced Sign.add_consts_authentic by Sign.declare_const; diff -r ff15f76741bd -r 119793c84647 src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Thu Oct 11 15:59:31 2007 +0200 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Thu Oct 11 16:05:23 2007 +0200 @@ -321,7 +321,7 @@ fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) ))); val ([def_thm], thy') = thy - |> Sign.add_consts_authentic [] [decl] + |> Sign.declare_const [] decl |> snd |> (PureThy.add_defs_i false o map Thm.no_attributes) [def]; in (defs @ [def_thm], thy') diff -r ff15f76741bd -r 119793c84647 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Thu Oct 11 15:59:31 2007 +0200 +++ b/src/HOL/Tools/datatype_package.ML Thu Oct 11 16:05:23 2007 +0200 @@ -517,7 +517,7 @@ end; val specify_consts = gen_specify_consts Sign.add_consts_i; -val specify_consts_authentic = gen_specify_consts (Sign.add_consts_authentic []); +val specify_consts_authentic = gen_specify_consts (fold (snd oo Sign.declare_const [])); structure DatatypeInterpretation = InterpretationFun(type T = string list val eq = op =); val interpretation = DatatypeInterpretation.interpretation; diff -r ff15f76741bd -r 119793c84647 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Thu Oct 11 15:59:31 2007 +0200 +++ b/src/HOL/Tools/res_axioms.ML Thu Oct 11 16:05:23 2007 +0200 @@ -77,12 +77,11 @@ val argsx = map (fn T => Free(gensym"vsk", T)) extraTs val args = argsx @ args0 val cT = extraTs ---> Ts ---> T - val c = Const (Sign.full_name thy cname, cT) val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) (*Forms a lambda-abstraction over the formal parameters*) val _ = Output.debug (fn () => "declaring the constant " ^ cname) - val thy' = - Sign.add_consts_authentic [Markup.property_internal] [(cname, cT, NoSyn)] thy + val (c, thy') = + Sign.declare_const [Markup.property_internal] (cname, cT, NoSyn) thy (*Theory is augmented with the constant, then its def*) val cdef = cname ^ "_def" val thy'' = Theory.add_defs_i true false [(cdef, equals cT $ c $ rhs)] thy' diff -r ff15f76741bd -r 119793c84647 src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Thu Oct 11 15:59:31 2007 +0200 +++ b/src/Pure/Isar/theory_target.ML Thu Oct 11 16:05:23 2007 +0200 @@ -195,10 +195,10 @@ fun const ((c, T), mx) thy = let val U = map #2 xs ---> T; - val t = Term.list_comb (Const (Sign.full_name thy c, U), map Free xs); val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx; val mx3 = if is_loc then NoSyn else mx1; - val thy' = Sign.add_consts_authentic (ContextPosition.properties_of lthy) [(c, U, mx3)] thy; + val (const, thy') = Sign.declare_const (ContextPosition.properties_of lthy) (c, U, mx3) thy; + val t = Term.list_comb (const, map Free xs); in (((c, mx2), t), thy') end; fun const_class (SOME class) ((c, _), mx) (_, t) = LocalTheory.raw_theory_result (Class.add_const_in_class class ((c, t), mx)) @@ -227,7 +227,7 @@ in lthy' |> fold2 (const_class some_class) decls abbrs - |> is_loc ? fold (internal_abbrev loc Syntax.default_mode) abbrs + |> is_loc ? fold (internal_abbrev loc Syntax.mode_default) abbrs |> LocalTheory.raw_theory (hide_abbrev some_class abbrs) (*FIXME abbreviations should never occur*) |> LocalDefs.add_defs defs diff -r ff15f76741bd -r 119793c84647 src/Pure/sign.ML --- a/src/Pure/sign.ML Thu Oct 11 15:59:31 2007 +0200 +++ b/src/Pure/sign.ML Thu Oct 11 16:05:23 2007 +0200 @@ -156,8 +156,7 @@ val simple_read_term: theory -> typ -> string -> term val read_term: theory -> string -> term val read_prop: theory -> string -> term - val add_consts_authentic: Markup.property list -> - (bstring * typ * mixfix) list -> theory -> theory + val declare_const: Markup.property list -> (bstring * typ * mixfix) -> theory -> term * theory val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory val add_abbrev: string -> Markup.property list -> bstring * term -> theory -> (term * term) * theory @@ -657,8 +656,8 @@ val add_modesyntax = gen_add_syntax Syntax.parse_typ; val add_modesyntax_i = gen_add_syntax (K I); -val add_syntax = add_modesyntax Syntax.default_mode; -val add_syntax_i = add_modesyntax_i Syntax.default_mode; +val add_syntax = add_modesyntax Syntax.mode_default; +val add_syntax_i = add_modesyntax_i Syntax.mode_default; val del_modesyntax = gen_syntax Syntax.remove_const_gram Syntax.parse_typ; val del_modesyntax_i = gen_syntax Syntax.remove_const_gram (K I); @@ -675,26 +674,30 @@ fun gen_add_consts prep_typ authentic tags raw_args thy = let - val prepT = Compress.typ thy o Logic.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy; + val prepT = Type.no_tvars o Term.no_dummyT o prep_typ thy; fun prep (raw_c, raw_T, raw_mx) = let val (c, mx) = Syntax.const_mixfix raw_c raw_mx; - val c' = if authentic then Syntax.constN ^ full_name thy c else c; + val full_c = full_name thy c; + val c' = if authentic then Syntax.constN ^ full_c else c; val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg => cat_error msg ("in declaration of constant " ^ quote c); - in ((c, T), (c', T, mx)) end; + val T' = Compress.typ thy (Logic.varifyT T); + in ((c, T'), (c', T', mx), Const (full_c, T)) end; val args = map prep raw_args; in thy |> map_consts (fold (Consts.declare authentic (naming_of thy) tags o #1) args) |> add_syntax_i (map #2 args) + |> pair (map #3 args) end; in -val add_consts = gen_add_consts read_typ false []; -val add_consts_i = gen_add_consts certify_typ false []; -val add_consts_authentic = gen_add_consts certify_typ true; +val add_consts = snd oo gen_add_consts read_typ false []; +val add_consts_i = snd oo gen_add_consts certify_typ false []; + +fun declare_const tags arg = gen_add_consts certify_typ true tags [arg] #>> the_single; end;