# HG changeset patch # User wenzelm # Date 1213383882 -7200 # Node ID bbf4cbc69243a2bde7b294134b7ce870a9984836 # Parent d4036ec60d46247c52556a354c9c7858d3ce5f6d map_const: soft version, no failure here; diff -r d4036ec60d46 -r bbf4cbc69243 src/Pure/Isar/proof_context.ML --- 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} diff -r d4036ec60d46 -r bbf4cbc69243 src/Pure/Syntax/syntax.ML --- 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 -> diff -r d4036ec60d46 -r bbf4cbc69243 src/Pure/sign.ML --- 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