# 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 =