Sorts.class_error: produce message only (formerly msg_class_error);
authorwenzelm
Sun Apr 13 16:40:08 2008 +0200 (2008-04-13)
changeset 26642454d11701fa4
parent 26641 cf67665296c2
child 26643 99f5407c05ef
Sorts.class_error: produce message only (formerly msg_class_error);
src/Pure/Isar/class.ML
src/Tools/code/code_funcgr.ML
     1.1 --- a/src/Pure/Isar/class.ML	Sun Apr 13 16:40:07 2008 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Sun Apr 13 16:40:08 2008 +0200
     1.3 @@ -707,7 +707,7 @@
     1.4                (Consts.typargs consts c_ty) sorts)
     1.5        | matchings _ = I
     1.6      val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
     1.7 -      handle Sorts.CLASS_ERROR e => Sorts.class_error pp e;
     1.8 +      handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e);
     1.9      val inst = map_type_tvar (fn (vi, _) => TVar (vi, the (Vartab.lookup tvartab vi)));
    1.10    in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end;
    1.11  
     2.1 --- a/src/Tools/code/code_funcgr.ML	Sun Apr 13 16:40:07 2008 +0200
     2.2 +++ b/src/Tools/code/code_funcgr.ML	Sun Apr 13 16:40:08 2008 +0200
     2.3 @@ -115,7 +115,7 @@
     2.4              val tys = Sign.const_typargs thy (c, ty);
     2.5              val sorts = map (snd o dest_TVar) (Sign.const_typargs thy (c, ty_decl));
     2.6            in fn tab => fold2 (curry (Sorts.meet_sort algebra)) tys sorts tab
     2.7 -            handle Sorts.CLASS_ERROR e => raise CLASS_ERROR ([c], Sorts.msg_class_error pp e ^ ",\n"
     2.8 +            handle Sorts.CLASS_ERROR e => raise CLASS_ERROR ([c], Sorts.class_error pp e ^ ",\n"
     2.9                ^ "for constant " ^ CodeUnit.string_of_const thy c
    2.10                ^ "\nin defining equations(s)\n"
    2.11                ^ (cat_lines o map string_of_thm) thms)