src/Pure/proofterm.ML
changeset 26328 b2d6f520172c
parent 23780 a0e7305dd0cb
child 26424 a6cad32a27b0
--- a/src/Pure/proofterm.ML	Wed Mar 19 07:20:31 2008 +0100
+++ b/src/Pure/proofterm.ML	Wed Mar 19 07:20:32 2008 +0100
@@ -421,12 +421,12 @@
 
 fun del_conflicting_tvars envT T = TermSubst.instantiateT
   (map_filter (fn ixnS as (_, S) =>
-     (Type.lookup (envT, ixnS); NONE) handle TYPE _ =>
+     (Type.lookup envT ixnS; NONE) handle TYPE _ =>
         SOME (ixnS, TFree ("'dummy", S))) (typ_tvars T)) T;
 
 fun del_conflicting_vars env t = TermSubst.instantiate
   (map_filter (fn ixnS as (_, S) =>
-     (Type.lookup (type_env env, ixnS); NONE) handle TYPE _ =>
+     (Type.lookup (type_env env) ixnS; NONE) handle TYPE _ =>
         SOME (ixnS, TFree ("'dummy", S))) (term_tvars t),
    map_filter (fn Var (ixnT as (_, T)) =>
      (Envir.lookup (env, ixnT); NONE) handle TYPE _ =>