src/Pure/theory.ML
changeset 28017 4919bd124a58
parent 26939 1035c89b4c02
child 28112 691993ef6abe
     1.1 --- a/src/Pure/theory.ML	Wed Aug 27 11:24:35 2008 +0200
     1.2 +++ b/src/Pure/theory.ML	Wed Aug 27 11:48:54 2008 +0200
     1.3 @@ -38,7 +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: Markup.property list -> bstring * typ * mixfix -> (string * typ) list ->
     1.8 +  val specify_const: Properties.T -> 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