src/Pure/theory.ML
changeset 25017 e82ab4962f80
parent 24981 4ec3f95190bf
child 25059 e6e0ee56a672
     1.1 --- a/src/Pure/theory.ML	Sat Oct 13 17:16:39 2007 +0200
     1.2 +++ b/src/Pure/theory.ML	Sat Oct 13 17:16:40 2007 +0200
     1.3 @@ -44,7 +44,8 @@
     1.4    val add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory
     1.5    val add_finals: bool -> string list -> theory -> theory
     1.6    val add_finals_i: bool -> term list -> theory -> theory
     1.7 -  val specify_const: Markup.property list -> bstring * typ * mixfix -> theory -> term * theory
     1.8 +  val specify_const: Markup.property list -> bstring * typ * mixfix -> (string * typ) list ->
     1.9 +   theory -> term * theory
    1.10    val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
    1.11  end
    1.12  
    1.13 @@ -266,6 +267,10 @@
    1.14      val name = if a = "" then (#1 lhs ^ " axiom") else a;
    1.15    in thy |> map_defs (dependencies thy false false name lhs rhs) end;
    1.16  
    1.17 +fun specify_const tags decl deps thy =
    1.18 +  let val (t as Const const, thy') = Sign.declare_const tags decl thy
    1.19 +  in (t, add_deps "" const deps thy') end;
    1.20 +
    1.21  
    1.22  (* check_overloading *)
    1.23  
    1.24 @@ -345,10 +350,6 @@
    1.25  
    1.26  end;
    1.27  
    1.28 -fun specify_const tags decl thy =
    1.29 -  let val (const, thy') = Sign.declare_const tags decl thy
    1.30 -  in (const, add_finals_i false [const] thy') end;
    1.31 -
    1.32  
    1.33  
    1.34  (** add oracle **)