src/Pure/type.ML
changeset 74232 1091880266e5
parent 66245 da3b0e848182
child 74233 9eff7c673b42
--- a/src/Pure/type.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/type.ML	Sat Sep 04 21:25:08 2021 +0200
@@ -446,7 +446,7 @@
   in match end;
 
 fun typ_instance tsig (T, U) =
-  (typ_match tsig (U, T) Vartab.empty; true) handle TYPE_MATCH => false;
+  (Vartab.build (typ_match tsig (U, T)); true) handle TYPE_MATCH => false;
 
 (*purely structural matching*)
 fun raw_match (TVar (v, S), T) subs =
@@ -474,7 +474,7 @@
 
 fun raw_instance (T, U) =
   if could_match (U, T) then
-    (raw_match (U, T) Vartab.empty; true) handle TYPE_MATCH => false
+    (Vartab.build (raw_match (U, T)); true) handle TYPE_MATCH => false
   else false;