# 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 *)