# HG changeset patch
# User wenzelm
# Date 1192111539 -7200
# Node ID 70111480b84b9450d624cfda6fcb089ba33b67b4
# Parent  8b4a029477219d4d68626bd4b72149e970360ac0
added specify_const;

diff -r 8b4a02947721 -r 70111480b84b src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu Oct 11 16:05:37 2007 +0200
+++ b/src/Pure/theory.ML	Thu Oct 11 16:05:39 2007 +0200
@@ -44,6 +44,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: Markup.property list -> bstring * typ * mixfix -> theory -> term * theory
   val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
 end
 
@@ -343,6 +344,10 @@
 
 end;
 
+fun specify_const tags decl thy =
+  let val (const, thy') = Sign.declare_const tags decl thy
+  in (const, add_finals_i false [const] thy') end;
+
 
 
 (** add oracle **)