src/Pure/sign.ML
changeset 24142 6f6b698b9def
parent 23963 c2ee97a963db
child 24233 5bec1b4149e7
     1.1 --- a/src/Pure/sign.ML	Fri Aug 03 16:28:20 2007 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri Aug 03 16:28:21 2007 +0200
     1.3 @@ -399,7 +399,7 @@
     1.4  val arity_number = Type.arity_number o tsig_of;
     1.5  fun arity_sorts thy = Type.arity_sorts (pp thy) (tsig_of thy);
     1.6  
     1.7 -fun certify cert = cert o tsig_of o Context.check_thy;
     1.8 +fun certify cert = cert o tsig_of;
     1.9  
    1.10  val certify_class      = certify Type.cert_class;
    1.11  val certify_sort       = certify Type.cert_sort;
    1.12 @@ -450,7 +450,6 @@
    1.13  
    1.14  fun certify' normalize prop pp consts thy tm =
    1.15    let
    1.16 -    val _ = Context.check_thy thy;
    1.17      val _ = check_vars tm;
    1.18      val tm' = Term.map_types (certify_typ thy) tm;
    1.19      val T = type_check pp tm';
    1.20 @@ -501,7 +500,6 @@
    1.21  fun read_sort' syn ctxt str =
    1.22    let
    1.23      val thy = ProofContext.theory_of ctxt;
    1.24 -    val _ = Context.check_thy thy;
    1.25      val S = Syntax.read_sort ctxt syn (intern_sort thy) str;
    1.26    in certify_sort thy S handle TYPE (msg, _, _) => error msg end;
    1.27  
    1.28 @@ -547,7 +545,6 @@
    1.29  fun gen_read_typ' cert syn ctxt def_sort str =
    1.30    let
    1.31      val thy = ProofContext.theory_of ctxt;
    1.32 -    val _ = Context.check_thy thy;
    1.33      val T = intern_tycons thy
    1.34        (Syntax.read_typ ctxt syn (get_sort thy def_sort) (intern_sort thy) str);
    1.35    in cert thy T handle TYPE (msg, _, _) => error msg end