equal
deleted
inserted
replaced
513 | remove_types (t $ u) = remove_types t $ remove_types u |
513 | remove_types (t $ u) = remove_types t $ remove_types u |
514 | remove_types (Const (s, _)) = Const (s, dummyT) |
514 | remove_types (Const (s, _)) = Const (s, dummyT) |
515 | remove_types t = t; |
515 | remove_types t = t; |
516 |
516 |
517 fun remove_types_env (Envir.Envir {maxidx, tenv, tyenv}) = |
517 fun remove_types_env (Envir.Envir {maxidx, tenv, tyenv}) = |
518 Envir.Envir {maxidx = maxidx, tenv = Vartab.map (apsnd remove_types) tenv, tyenv = tyenv}; |
518 Envir.Envir {maxidx = maxidx, tenv = Vartab.map (K (apsnd remove_types)) tenv, tyenv = tyenv}; |
519 |
519 |
520 fun norm_proof' env prf = norm_proof (remove_types_env env) prf; |
520 fun norm_proof' env prf = norm_proof (remove_types_env env) prf; |
521 |
521 |
522 |
522 |
523 (**** substitution of bound variables ****) |
523 (**** substitution of bound variables ****) |