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