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