test_classrel/arity improve error reporting; tuned;
authorwenzelm
Fri May 21 21:23:12 2004 +0200 (2004-05-21 ago)
changeset 14785d88f4c8f0591
parent 14784 e65d77313a94
child 14786 24a7bc97a27a
test_classrel/arity improve error reporting; tuned;
src/Pure/axclass.ML
     1.1 --- a/src/Pure/axclass.ML	Fri May 21 21:22:42 2004 +0200
     1.2 +++ b/src/Pure/axclass.ML	Fri May 21 21:23:12 2004 +0200
     1.3 @@ -255,7 +255,7 @@
     1.4          [] => []
     1.5        | [(_, S)] => if Sign.subsort class_sign ([class], S) then S else err_bad_axsort name class
     1.6        | _ => err_bad_tfrees name);
     1.7 -    val axS = Sign.norm_sort class_sign (logicC :: flat (map axm_sort axms));
     1.8 +    val axS = Sign.certify_sort class_sign (logicC :: flat (map axm_sort axms));
     1.9  
    1.10      val int_axm = Logic.close_form o map_term_tfrees (K (aT axS));
    1.11      fun inclass c = Logic.mk_inclass (aT axS, c);
    1.12 @@ -363,20 +363,14 @@
    1.13  
    1.14  fun read_class sg c = Sign.certify_class sg (Sign.intern_class sg c);
    1.15  
    1.16 -fun cert_classrel sg cc = Library.pairself (Sign.certify_class sg) cc;
    1.17 -fun read_classrel sg cc = Library.pairself (read_class sg) cc;
    1.18 +fun test_classrel sg cc = (Type.add_classrel [cc] (Sign.tsig_of sg); cc);
    1.19 +fun cert_classrel sg = test_classrel sg o Library.pairself (Sign.certify_class sg);
    1.20 +fun read_classrel sg = test_classrel sg o Library.pairself (read_class sg);
    1.21  
    1.22 -fun check_tycon sg t =
    1.23 -  let val {tycons, abbrs, ...} = Type.rep_tsig (Sign.tsig_of sg) in
    1.24 -    if is_some (Symtab.lookup (abbrs, t)) then
    1.25 -      error ("Illegal type abbreviation: " ^ quote t)
    1.26 -    else if is_none (Symtab.lookup (tycons, t)) then
    1.27 -      error ("Undeclared type constructor: " ^ quote t)
    1.28 -    else t
    1.29 -  end;
    1.30 +fun test_arity sg ar = (Type.add_arities [ar] (Sign.tsig_of sg); ar);
    1.31  
    1.32  fun prep_arity prep_tycon prep_sort prep_x sg (t, Ss, x) =
    1.33 -  (check_tycon sg (prep_tycon sg t), map (prep_sort sg) Ss, prep_x sg x);
    1.34 +  test_arity sg (prep_tycon sg t, map (prep_sort sg) Ss, prep_x sg x);  
    1.35  
    1.36  val read_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.read_sort;
    1.37  val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort;