src/Pure/proofterm.ML
changeset 51700 c8f2bad67dbb
parent 51100 18daa3380ff7
child 52424 77075c576d4c
     1.1 --- a/src/Pure/proofterm.ML	Fri Apr 12 12:20:51 2013 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Fri Apr 12 14:54:14 2013 +0200
     1.3 @@ -468,7 +468,7 @@
     1.4       (Type.lookup (Envir.type_env env) ixnS; NONE) handle TYPE _ =>
     1.5          SOME (ixnS, TFree ("'dummy", S))) (Term.add_tvars t []),
     1.6     map_filter (fn (ixnT as (_, T)) =>
     1.7 -     (Envir.lookup (env, ixnT); NONE) handle TYPE _ =>
     1.8 +     (Envir.lookup env ixnT; NONE) handle TYPE _ =>
     1.9          SOME (ixnT, Free ("dummy", T))) (Term.add_vars t [])) t;
    1.10  
    1.11  fun norm_proof env =