map_const: soft version, no failure here;
authorwenzelm
Fri Jun 13 21:04:42 2008 +0200 (2008-06-13)
changeset 27195bbf4cbc69243
parent 27194 d4036ec60d46
child 27196 ef2f01da7a12
map_const: soft version, no failure here;
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/syntax.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Fri Jun 13 21:04:12 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Jun 13 21:04:42 2008 +0200
     1.3 @@ -542,7 +542,8 @@
     1.4  fun term_context ctxt =
     1.5    let val thy = theory_of ctxt in
     1.6     {get_sort = Sign.get_sort thy (Variable.def_sort ctxt),
     1.7 -    map_const = try (#1 o Term.dest_Const o read_const_proper ctxt),
     1.8 +    map_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt a)))
     1.9 +      handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
    1.10      map_free = intern_skolem ctxt (Variable.def_type ctxt false),
    1.11      map_type = Sign.intern_tycons thy,
    1.12      map_sort = Sign.intern_sort thy}
     2.1 --- a/src/Pure/Syntax/syntax.ML	Fri Jun 13 21:04:12 2008 +0200
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Jun 13 21:04:42 2008 +0200
     2.3 @@ -42,7 +42,7 @@
     2.4    val read: Proof.context -> (string -> bool) -> syntax -> typ -> string -> term list
     2.5    val standard_parse_term: Pretty.pp -> (term -> string option) ->
     2.6      (((string * int) * sort) list -> string * int -> Term.sort) ->
     2.7 -    (string -> string option) -> (string -> string option) ->
     2.8 +    (string -> bool * string) -> (string -> string option) ->
     2.9      (typ -> typ) -> (sort -> sort) -> Proof.context ->
    2.10      (string -> bool) -> syntax -> typ -> string -> term
    2.11    val standard_parse_typ: Proof.context -> syntax ->
     3.1 --- a/src/Pure/sign.ML	Fri Jun 13 21:04:12 2008 +0200
     3.2 +++ b/src/Pure/sign.ML	Fri Jun 13 21:04:42 2008 +0200
     3.3 @@ -499,7 +499,8 @@
     3.4        handle TYPE (msg, _, _) => error msg;
     3.5  
     3.6      fun check T t = (singleton (fst o infer) (t, T); NONE) handle ERROR msg => SOME msg;
     3.7 -    val map_const = try (#1 o Term.dest_Const o Consts.read_const consts);
     3.8 +    fun map_const a = (true, #1 (Term.dest_Const (Consts.read_const consts a)))
     3.9 +      handle ERROR _ => (false, Consts.intern consts a);
    3.10      fun read T = Syntax.standard_parse_term pp (check T) (get_sort thy def_sort) map_const map_free
    3.11          (intern_tycons thy) (intern_sort thy) ctxt is_logtype syn T;
    3.12    in