# HG changeset patch
# User haftmann
# Date 1203678115 -3600
# Node ID ac2ce7242eae696cf2e0dfaaafddfb11d5fca9d1
# Parent  91e0999b075fc47c7bb30dae12bfbff78ae25777
added further interface for reading constants

diff -r 91e0999b075f -r ac2ce7242eae src/Pure/Isar/code_unit.ML
--- a/src/Pure/Isar/code_unit.ML	Fri Feb 22 12:01:54 2008 +0100
+++ b/src/Pure/Isar/code_unit.ML	Fri Feb 22 12:01:55 2008 +0100
@@ -23,6 +23,7 @@
   val string_of_typ: theory -> typ -> string
   val string_of_const: theory -> string -> string
   val no_args: theory -> string -> int
+  val check_const: theory -> term -> string
   val read_bare_const: theory -> string -> string * typ
   val read_const: theory -> string -> string
   val read_const_exprs: theory -> (string list -> string list)
@@ -68,13 +69,13 @@
 
 (* reading constants as terms and wildcards pattern *)
 
-fun read_bare_const thy raw_t =
-  let
-    val t = Syntax.read_term_global thy raw_t;
-  in case try dest_Const t
-   of SOME c_ty => c_ty
-    | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
-  end;
+fun check_bare_const thy t = case try dest_Const t
+ of SOME c_ty => c_ty
+  | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t);
+
+fun check_const thy = AxClass.unoverload_const thy o check_bare_const thy;
+
+fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy;
 
 fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;