src/Pure/theory.ML
changeset 28112 691993ef6abe
parent 28017 4919bd124a58
child 28290 4cc2b6046258
     1.1 --- a/src/Pure/theory.ML	Wed Sep 03 17:47:34 2008 +0200
     1.2 +++ b/src/Pure/theory.ML	Wed Sep 03 17:47:35 2008 +0200
     1.3 @@ -38,8 +38,7 @@
     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: Properties.T -> bstring * typ * mixfix -> (string * typ) list ->
     1.8 -   theory -> term * theory
     1.9 +  val specify_const: Properties.T -> (Name.binding * typ) * mixfix -> theory -> term * theory
    1.10    val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
    1.11  end
    1.12  
    1.13 @@ -241,9 +240,9 @@
    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 +fun specify_const tags decl thy =
    1.19    let val (t as Const const, thy') = Sign.declare_const tags decl thy
    1.20 -  in (t, add_deps "" const deps thy') end;
    1.21 +  in (t, add_deps "" const [] thy') end;
    1.22  
    1.23  
    1.24  (* check_overloading *)