added specify_const;
authorwenzelm
Thu Oct 11 16:05:39 2007 +0200 (2007-10-11)
changeset 2496670111480b84b
parent 24965 8b4a02947721
child 24967 68c5c62bed13
added specify_const;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Thu Oct 11 16:05:37 2007 +0200
     1.2 +++ b/src/Pure/theory.ML	Thu Oct 11 16:05:39 2007 +0200
     1.3 @@ -44,6 +44,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 -> theory -> term * theory
     1.8    val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
     1.9  end
    1.10  
    1.11 @@ -343,6 +344,10 @@
    1.12  
    1.13  end;
    1.14  
    1.15 +fun specify_const tags decl thy =
    1.16 +  let val (const, thy') = Sign.declare_const tags decl thy
    1.17 +  in (const, add_finals_i false [const] thy') end;
    1.18 +
    1.19  
    1.20  
    1.21  (** add oracle **)