--- a/src/Pure/Isar/proof_context.ML Fri Jun 13 21:04:12 2008 +0200
+++ b/src/Pure/Isar/proof_context.ML Fri Jun 13 21:04:42 2008 +0200
@@ -542,7 +542,8 @@
fun term_context ctxt =
let val thy = theory_of ctxt in
{get_sort = Sign.get_sort thy (Variable.def_sort ctxt),
- map_const = try (#1 o Term.dest_Const o read_const_proper ctxt),
+ map_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt a)))
+ handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
map_free = intern_skolem ctxt (Variable.def_type ctxt false),
map_type = Sign.intern_tycons thy,
map_sort = Sign.intern_sort thy}
--- a/src/Pure/Syntax/syntax.ML Fri Jun 13 21:04:12 2008 +0200
+++ b/src/Pure/Syntax/syntax.ML Fri Jun 13 21:04:42 2008 +0200
@@ -42,7 +42,7 @@
val read: Proof.context -> (string -> bool) -> syntax -> typ -> string -> term list
val standard_parse_term: Pretty.pp -> (term -> string option) ->
(((string * int) * sort) list -> string * int -> Term.sort) ->
- (string -> string option) -> (string -> string option) ->
+ (string -> bool * string) -> (string -> string option) ->
(typ -> typ) -> (sort -> sort) -> Proof.context ->
(string -> bool) -> syntax -> typ -> string -> term
val standard_parse_typ: Proof.context -> syntax ->
--- a/src/Pure/sign.ML Fri Jun 13 21:04:12 2008 +0200
+++ b/src/Pure/sign.ML Fri Jun 13 21:04:42 2008 +0200
@@ -499,7 +499,8 @@
handle TYPE (msg, _, _) => error msg;
fun check T t = (singleton (fst o infer) (t, T); NONE) handle ERROR msg => SOME msg;
- val map_const = try (#1 o Term.dest_Const o Consts.read_const consts);
+ fun map_const a = (true, #1 (Term.dest_Const (Consts.read_const consts a)))
+ handle ERROR _ => (false, Consts.intern consts a);
fun read T = Syntax.standard_parse_term pp (check T) (get_sort thy def_sort) map_const map_free
(intern_tycons thy) (intern_sort thy) ctxt is_logtype syn T;
in