src/Pure/sign.ML
changeset 16723 9a9c034f1d57
parent 16655 3e4d726aaed1
child 16894 40f80823b451
     1.1 --- a/src/Pure/sign.ML	Wed Jul 06 20:00:29 2005 +0200
     1.2 +++ b/src/Pure/sign.ML	Wed Jul 06 20:00:31 2005 +0200
     1.3 @@ -352,7 +352,7 @@
     1.4  
     1.5  (* certify wrt. type signature *)
     1.6  
     1.7 -fun certify cert = cert o tsig_of o Context.check_thy "Sign.certify";
     1.8 +fun certify cert = cert o tsig_of o Context.check_thy;
     1.9  
    1.10  val certify_class      = certify Type.cert_class;
    1.11  val certify_sort       = certify Type.cert_sort;
    1.12 @@ -397,7 +397,7 @@
    1.13  
    1.14  fun certify_term pp thy tm =
    1.15    let
    1.16 -    val _ = Context.check_thy "Sign.certify_term" thy;
    1.17 +    val _ = Context.check_thy thy;
    1.18  
    1.19      val tm' = map_term_types (certify_typ thy) tm;
    1.20      val tm' = if tm = tm' then tm else tm';  (*avoid copying of already normal term*)
    1.21 @@ -439,7 +439,7 @@
    1.22  
    1.23  fun read_sort' syn thy str =
    1.24    let
    1.25 -    val _ = Context.check_thy "Sign.read_sort'" thy;
    1.26 +    val _ = Context.check_thy thy;
    1.27      val S = intern_sort thy (Syntax.read_sort thy syn str);
    1.28    in certify_sort thy S handle TYPE (msg, _, _) => error msg end;
    1.29  
    1.30 @@ -452,7 +452,7 @@
    1.31  
    1.32  fun gen_read_typ' cert syn (thy, def_sort) str =
    1.33    let
    1.34 -    val _ = Context.check_thy "Sign.gen_read_typ'" thy;
    1.35 +    val _ = Context.check_thy thy;
    1.36      val get_sort = TypeInfer.get_sort (tsig_of thy) def_sort (intern_sort thy);
    1.37      val T = intern_tycons thy (Syntax.read_typ thy syn get_sort (intern_sort thy) str);
    1.38    in cert thy T handle TYPE (msg, _, _) => error msg end