src/Pure/sign.ML

 (* certify wrt. type signature *)
 
 val arity_number = Type.arity_number o tsig_of;
 fun arity_sorts thy = Type.arity_sorts (pp thy) (tsig_of thy);
 
-fun certify cert = cert o tsig_of o Context.check_thy;
+fun certify cert = cert o tsig_of;
 
 val certify_class      = certify Type.cert_class;
 val certify_sort       = certify Type.cert_sort;
 val certify_typ        = certify Type.cert_typ;
 val certify_typ_syntax = certify Type.cert_typ_syntax;

 
 in
 
 fun certify' normalize prop pp consts thy tm =
   let
-    val _ = Context.check_thy thy;
     val _ = check_vars tm;
     val tm' = Term.map_types (certify_typ thy) tm;
     val T = type_check pp tm';
     val _ = if prop andalso T <> propT then err "Term not of type prop" else ();
     val tm'' = Consts.certify pp (tsig_of thy) consts tm';

   handle TYPE (msg, _, _) => error msg;
 
 fun read_sort' syn ctxt str =
   let
     val thy = ProofContext.theory_of ctxt;
-    val _ = Context.check_thy thy;
     val S = Syntax.read_sort ctxt syn (intern_sort thy) str;
   in certify_sort thy S handle TYPE (msg, _, _) => error msg end;
 
 fun read_sort thy str = read_sort' (syn_of thy) (ProofContext.init thy) str;
 

 local
 
 fun gen_read_typ' cert syn ctxt def_sort str =
   let
     val thy = ProofContext.theory_of ctxt;
-    val _ = Context.check_thy thy;
     val T = intern_tycons thy
       (Syntax.read_typ ctxt syn (get_sort thy def_sort) (intern_sort thy) str);
   in cert thy T handle TYPE (msg, _, _) => error msg end
   handle ERROR msg => cat_error msg ("The error(s) above occurred in type " ^ quote str);