# 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;