src/Pure/sign.ML
changeset 27195 bbf4cbc69243
parent 26978 fd4b4ecf935e
child 27205 56c96c02ab79
     1.1 --- a/src/Pure/sign.ML	Fri Jun 13 21:04:12 2008 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri Jun 13 21:04:42 2008 +0200
     1.3 @@ -499,7 +499,8 @@
     1.4        handle TYPE (msg, _, _) => error msg;
     1.5  
     1.6      fun check T t = (singleton (fst o infer) (t, T); NONE) handle ERROR msg => SOME msg;
     1.7 -    val map_const = try (#1 o Term.dest_Const o Consts.read_const consts);
     1.8 +    fun map_const a = (true, #1 (Term.dest_Const (Consts.read_const consts a)))
     1.9 +      handle ERROR _ => (false, Consts.intern consts a);
    1.10      fun read T = Syntax.standard_parse_term pp (check T) (get_sort thy def_sort) map_const map_free
    1.11          (intern_tycons thy) (intern_sort thy) ctxt is_logtype syn T;
    1.12    in