src/Pure/Isar/class.ML
changeset 27089 480f19078b65
parent 26995 2511a72dd73c
child 27281 b457537e789a
     1.1 --- a/src/Pure/Isar/class.ML	Fri Jun 06 18:36:35 2008 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Sat Jun 07 19:18:38 2008 +0200
     1.3 @@ -714,7 +714,8 @@
     1.4        | matchings _ = I
     1.5      val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
     1.6        handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e);
     1.7 -    val inst = map_type_tvar (fn (vi, _) => TVar (vi, the (Vartab.lookup tvartab vi)));
     1.8 +    val inst = map_type_tvar
     1.9 +      (fn (vi, sort) => TVar (vi, the_default sort (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  
    1.12  fun init_instantiation (tycos, vs, sort) thy =