Theory.specify_const: added deps argument;
authorwenzelm
Sat Oct 13 17:16:40 2007 +0200 (2007-10-13)
changeset 25017e82ab4962f80
parent 25016 2bcac52d7abc
child 25018 fac2ceba75b4
Theory.specify_const: added deps argument;
src/HOL/Tools/function_package/size.ML
src/Pure/theory.ML
     1.1 --- a/src/HOL/Tools/function_package/size.ML	Sat Oct 13 17:16:39 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/size.ML	Sat Oct 13 17:16:40 2007 +0200
     1.3 @@ -156,7 +156,7 @@
     1.4        (map (fn T => name_of_typ T ^ size_suffix) (Library.drop (head_len, recTs)));
     1.5  
     1.6      val thy' = thy |> fold (fn (s, T) =>
     1.7 -        snd o Theory.specify_const [] (Sign.base_name s, T --> HOLogic.natT, NoSyn))
     1.8 +        snd o Theory.specify_const [] (Sign.base_name s, T --> HOLogic.natT, NoSyn) [])
     1.9        (size_names ~~ Library.drop (head_len, recTs))
    1.10      val size_axs = make_size head_len descr' sorts recTs thy';
    1.11    in
     2.1 --- a/src/Pure/theory.ML	Sat Oct 13 17:16:39 2007 +0200
     2.2 +++ b/src/Pure/theory.ML	Sat Oct 13 17:16:40 2007 +0200
     2.3 @@ -44,7 +44,8 @@
     2.4    val add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory
     2.5    val add_finals: bool -> string list -> theory -> theory
     2.6    val add_finals_i: bool -> term list -> theory -> theory
     2.7 -  val specify_const: Markup.property list -> bstring * typ * mixfix -> theory -> term * theory
     2.8 +  val specify_const: Markup.property list -> bstring * typ * mixfix -> (string * typ) list ->
     2.9 +   theory -> term * theory
    2.10    val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
    2.11  end
    2.12  
    2.13 @@ -266,6 +267,10 @@
    2.14      val name = if a = "" then (#1 lhs ^ " axiom") else a;
    2.15    in thy |> map_defs (dependencies thy false false name lhs rhs) end;
    2.16  
    2.17 +fun specify_const tags decl deps thy =
    2.18 +  let val (t as Const const, thy') = Sign.declare_const tags decl thy
    2.19 +  in (t, add_deps "" const deps thy') end;
    2.20 +
    2.21  
    2.22  (* check_overloading *)
    2.23  
    2.24 @@ -345,10 +350,6 @@
    2.25  
    2.26  end;
    2.27  
    2.28 -fun specify_const tags decl thy =
    2.29 -  let val (const, thy') = Sign.declare_const tags decl thy
    2.30 -  in (const, add_finals_i false [const] thy') end;
    2.31 -
    2.32  
    2.33  
    2.34  (** add oracle **)