replaced Sign.add_consts_authentic by Sign.declare_const;
authorwenzelm
Thu Oct 11 16:05:23 2007 +0200 (2007-10-11)
changeset 24959119793c84647
parent 24958 ff15f76741bd
child 24960 39d1dd215d73
replaced Sign.add_consts_authentic by Sign.declare_const;
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/res_axioms.ML
src/Pure/Isar/theory_target.ML
src/Pure/sign.ML
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu Oct 11 15:59:31 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Thu Oct 11 16:05:23 2007 +0200
     1.3 @@ -321,7 +321,7 @@
     1.4                  fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) )));
     1.5            val ([def_thm], thy') =
     1.6              thy
     1.7 -            |> Sign.add_consts_authentic [] [decl]
     1.8 +            |> Sign.declare_const [] decl |> snd
     1.9              |> (PureThy.add_defs_i false o map Thm.no_attributes) [def];
    1.10  
    1.11          in (defs @ [def_thm], thy')
     2.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Oct 11 15:59:31 2007 +0200
     2.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Oct 11 16:05:23 2007 +0200
     2.3 @@ -517,7 +517,7 @@
     2.4    end;
     2.5  
     2.6  val specify_consts = gen_specify_consts Sign.add_consts_i;
     2.7 -val specify_consts_authentic = gen_specify_consts (Sign.add_consts_authentic []);
     2.8 +val specify_consts_authentic = gen_specify_consts (fold (snd oo Sign.declare_const []));
     2.9  
    2.10  structure DatatypeInterpretation = InterpretationFun(type T = string list val eq = op =);
    2.11  val interpretation = DatatypeInterpretation.interpretation;
     3.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Oct 11 15:59:31 2007 +0200
     3.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Oct 11 16:05:23 2007 +0200
     3.3 @@ -77,12 +77,11 @@
     3.4                  val argsx = map (fn T => Free(gensym"vsk", T)) extraTs
     3.5                  val args = argsx @ args0
     3.6                  val cT = extraTs ---> Ts ---> T
     3.7 -                val c = Const (Sign.full_name thy cname, cT)
     3.8                  val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
     3.9                          (*Forms a lambda-abstraction over the formal parameters*)
    3.10                  val _ = Output.debug (fn () => "declaring the constant " ^ cname)
    3.11 -                val thy' =
    3.12 -                  Sign.add_consts_authentic [Markup.property_internal] [(cname, cT, NoSyn)] thy
    3.13 +                val (c, thy') =
    3.14 +                  Sign.declare_const [Markup.property_internal] (cname, cT, NoSyn) thy
    3.15                             (*Theory is augmented with the constant, then its def*)
    3.16                  val cdef = cname ^ "_def"
    3.17                  val thy'' = Theory.add_defs_i true false [(cdef, equals cT $ c $ rhs)] thy'
     4.1 --- a/src/Pure/Isar/theory_target.ML	Thu Oct 11 15:59:31 2007 +0200
     4.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Oct 11 16:05:23 2007 +0200
     4.3 @@ -195,10 +195,10 @@
     4.4      fun const ((c, T), mx) thy =
     4.5        let
     4.6          val U = map #2 xs ---> T;
     4.7 -        val t = Term.list_comb (Const (Sign.full_name thy c, U), map Free xs);
     4.8          val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx;
     4.9          val mx3 = if is_loc then NoSyn else mx1;
    4.10 -        val thy' = Sign.add_consts_authentic (ContextPosition.properties_of lthy) [(c, U, mx3)] thy;
    4.11 +        val (const, thy') = Sign.declare_const (ContextPosition.properties_of lthy) (c, U, mx3) thy;
    4.12 +        val t = Term.list_comb (const, map Free xs);
    4.13        in (((c, mx2), t), thy') end;
    4.14      fun const_class (SOME class) ((c, _), mx) (_, t) =
    4.15            LocalTheory.raw_theory_result (Class.add_const_in_class class ((c, t), mx))
    4.16 @@ -227,7 +227,7 @@
    4.17    in
    4.18      lthy'
    4.19      |> fold2 (const_class some_class) decls abbrs
    4.20 -    |> is_loc ? fold (internal_abbrev loc Syntax.default_mode) abbrs
    4.21 +    |> is_loc ? fold (internal_abbrev loc Syntax.mode_default) abbrs
    4.22      |> LocalTheory.raw_theory (hide_abbrev some_class abbrs)
    4.23          (*FIXME abbreviations should never occur*)
    4.24      |> LocalDefs.add_defs defs
     5.1 --- a/src/Pure/sign.ML	Thu Oct 11 15:59:31 2007 +0200
     5.2 +++ b/src/Pure/sign.ML	Thu Oct 11 16:05:23 2007 +0200
     5.3 @@ -156,8 +156,7 @@
     5.4    val simple_read_term: theory -> typ -> string -> term
     5.5    val read_term: theory -> string -> term
     5.6    val read_prop: theory -> string -> term
     5.7 -  val add_consts_authentic: Markup.property list ->
     5.8 -    (bstring * typ * mixfix) list -> theory -> theory
     5.9 +  val declare_const: Markup.property list -> (bstring * typ * mixfix) -> theory -> term * theory
    5.10    val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
    5.11    val add_abbrev: string -> Markup.property list ->
    5.12      bstring * term -> theory -> (term * term) * theory
    5.13 @@ -657,8 +656,8 @@
    5.14  
    5.15  val add_modesyntax = gen_add_syntax Syntax.parse_typ;
    5.16  val add_modesyntax_i = gen_add_syntax (K I);
    5.17 -val add_syntax = add_modesyntax Syntax.default_mode;
    5.18 -val add_syntax_i = add_modesyntax_i Syntax.default_mode;
    5.19 +val add_syntax = add_modesyntax Syntax.mode_default;
    5.20 +val add_syntax_i = add_modesyntax_i Syntax.mode_default;
    5.21  val del_modesyntax = gen_syntax Syntax.remove_const_gram Syntax.parse_typ;
    5.22  val del_modesyntax_i = gen_syntax Syntax.remove_const_gram (K I);
    5.23  
    5.24 @@ -675,26 +674,30 @@
    5.25  
    5.26  fun gen_add_consts prep_typ authentic tags raw_args thy =
    5.27    let
    5.28 -    val prepT = Compress.typ thy o Logic.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
    5.29 +    val prepT = Type.no_tvars o Term.no_dummyT o prep_typ thy;
    5.30      fun prep (raw_c, raw_T, raw_mx) =
    5.31        let
    5.32          val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
    5.33 -        val c' = if authentic then Syntax.constN ^ full_name thy c else c;
    5.34 +        val full_c = full_name thy c;
    5.35 +        val c' = if authentic then Syntax.constN ^ full_c else c;
    5.36          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
    5.37            cat_error msg ("in declaration of constant " ^ quote c);
    5.38 -      in ((c, T), (c', T, mx)) end;
    5.39 +        val T' = Compress.typ thy (Logic.varifyT T);
    5.40 +      in ((c, T'), (c', T', mx), Const (full_c, T)) end;
    5.41      val args = map prep raw_args;
    5.42    in
    5.43      thy
    5.44      |> map_consts (fold (Consts.declare authentic (naming_of thy) tags o #1) args)
    5.45      |> add_syntax_i (map #2 args)
    5.46 +    |> pair (map #3 args)
    5.47    end;
    5.48  
    5.49  in
    5.50  
    5.51 -val add_consts = gen_add_consts read_typ false [];
    5.52 -val add_consts_i = gen_add_consts certify_typ false [];
    5.53 -val add_consts_authentic = gen_add_consts certify_typ true;
    5.54 +val add_consts = snd oo gen_add_consts read_typ false [];
    5.55 +val add_consts_i = snd oo gen_add_consts certify_typ false [];
    5.56 +
    5.57 +fun declare_const tags arg = gen_add_consts certify_typ true tags [arg] #>> the_single;
    5.58  
    5.59  end;
    5.60