src/Pure/Isar/class.ML
changeset 26642 454d11701fa4
parent 26628 63306cb94313
child 26730 bbb5e6904d78
     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