map_const: soft version, no failure here;

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