# HG changeset patch # User haftmann # Date 1212859118 -7200 # Node ID 480f19078b6542e9d1c6fdf4c79f6cb42dd491a3 # Parent 891a3c9db9e1302b7d7790339962133456c3cd5e fixed wrong treatment of type variables in instantiation target diff -r 891a3c9db9e1 -r 480f19078b65 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Fri Jun 06 18:36:35 2008 +0200 +++ b/src/Pure/Isar/class.ML Sat Jun 07 19:18:38 2008 +0200 @@ -714,7 +714,8 @@ | matchings _ = I val tvartab = (fold o fold_aterms) matchings ts Vartab.empty handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e); - val inst = map_type_tvar (fn (vi, _) => TVar (vi, the (Vartab.lookup tvartab vi))); + val inst = map_type_tvar + (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi))); in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end; fun init_instantiation (tycos, vs, sort) thy =