src/Pure/sign.ML
changeset 25476 03da46cfab9e
parent 25458 ba8f5e4fa336
child 26268 80aaf4d034be
     1.1 --- a/src/Pure/sign.ML	Tue Nov 27 16:48:37 2007 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Nov 27 16:48:38 2007 +0100
     1.3 @@ -537,8 +537,7 @@
     1.4          (try (Consts.the_constraint consts)) def_type used ~1 (SOME freeze) args |>> map fst
     1.5        handle TYPE (msg, _, _) => error msg;
     1.6  
     1.7 -    fun check T t = Exn.Result (singleton (fst o infer) (t, T))
     1.8 -      handle ERROR msg => Exn.Exn (ERROR msg);
     1.9 +    fun check T t = (singleton (fst o infer) (t, T); NONE) handle ERROR msg => SOME msg;
    1.10      val map_const = try (#1 o Term.dest_Const o Consts.read_const consts);
    1.11      fun read T = Syntax.standard_parse_term pp (check T) (get_sort thy def_sort) map_const map_free
    1.12          (intern_tycons thy) (intern_sort thy) ctxt is_logtype syn T;