Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed wrong treatment of type variables in instantiation target
authorhaftmann
Sat, 07 Jun 2008 19:18:38 +0200
changeset 27089 480f19078b65
parent 27088 891a3c9db9e1
child 27090 2f45c1b1b05d
fixed wrong treatment of type variables in instantiation target
src/Pure/Isar/class.ML file | annotate | diff | comparison | revisions 
--- 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 =
isabelle