# HG changeset patch
# User wenzelm
# Date 1192288600 -7200
# Node ID e82ab4962f806f84379d1ae082ab7d5b475c01dc
# Parent  2bcac52d7abc796db3c1c28988de7e07e4a5585f
Theory.specify_const: added deps argument;

diff -r 2bcac52d7abc -r e82ab4962f80 src/HOL/Tools/function_package/size.ML
--- a/src/HOL/Tools/function_package/size.ML	Sat Oct 13 17:16:39 2007 +0200
+++ b/src/HOL/Tools/function_package/size.ML	Sat Oct 13 17:16:40 2007 +0200
@@ -156,7 +156,7 @@
       (map (fn T => name_of_typ T ^ size_suffix) (Library.drop (head_len, recTs)));
 
     val thy' = thy |> fold (fn (s, T) =>
-        snd o Theory.specify_const [] (Sign.base_name s, T --> HOLogic.natT, NoSyn))
+        snd o Theory.specify_const [] (Sign.base_name s, T --> HOLogic.natT, NoSyn) [])
       (size_names ~~ Library.drop (head_len, recTs))
     val size_axs = make_size head_len descr' sorts recTs thy';
   in
diff -r 2bcac52d7abc -r e82ab4962f80 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sat Oct 13 17:16:39 2007 +0200
+++ b/src/Pure/theory.ML	Sat Oct 13 17:16:40 2007 +0200
@@ -44,7 +44,8 @@
   val add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory
   val add_finals: bool -> string list -> theory -> theory
   val add_finals_i: bool -> term list -> theory -> theory
-  val specify_const: Markup.property list -> bstring * typ * mixfix -> theory -> term * theory
+  val specify_const: Markup.property list -> bstring * typ * mixfix -> (string * typ) list ->
+   theory -> term * theory
   val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
 end
 
@@ -266,6 +267,10 @@
     val name = if a = "" then (#1 lhs ^ " axiom") else a;
   in thy |> map_defs (dependencies thy false false name lhs rhs) end;
 
+fun specify_const tags decl deps thy =
+  let val (t as Const const, thy') = Sign.declare_const tags decl thy
+  in (t, add_deps "" const deps thy') end;
+
 
 (* check_overloading *)
 
@@ -345,10 +350,6 @@
 
 end;
 
-fun specify_const tags decl thy =
-  let val (const, thy') = Sign.declare_const tags decl thy
-  in (const, add_finals_i false [const] thy') end;
-
 
 
 (** add oracle **)