# HG changeset patch
# User wenzelm
# Date 1220456855 -7200
# Node ID 691993ef6abed63f1b1b52d9967a98a852b8ce40
# Parent  ea22fd4685fbc5e90075874eba5af35c4bc28e12
simplified specify_const: canonical args, global deps;

diff -r ea22fd4685fb -r 691993ef6abe src/Pure/theory.ML
--- a/src/Pure/theory.ML	Wed Sep 03 17:47:34 2008 +0200
+++ b/src/Pure/theory.ML	Wed Sep 03 17:47:35 2008 +0200
@@ -38,8 +38,7 @@
   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: Properties.T -> bstring * typ * mixfix -> (string * typ) list ->
-   theory -> term * theory
+  val specify_const: Properties.T -> (Name.binding * typ) * mixfix -> theory -> term * theory
   val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
 end
 
@@ -241,9 +240,9 @@
     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 =
+fun specify_const tags decl thy =
   let val (t as Const const, thy') = Sign.declare_const tags decl thy
-  in (t, add_deps "" const deps thy') end;
+  in (t, add_deps "" const [] thy') end;
 
 
 (* check_overloading *)