changeset 79409 | e1895596e1b9 |
parent 79407 | c6c2e41cac1c |
child 79411 | 700d4f16b5f2 |
--- a/src/Pure/Proof/extraction.ML Sun Dec 31 18:49:00 2023 +0100 +++ b/src/Pure/Proof/extraction.ML Sun Dec 31 19:24:37 2023 +0100 @@ -390,7 +390,7 @@ val cs = maps (fn T => map (pair T) S) Ts; val constraints' = map Logic.mk_of_class cs; val typ_map = Type.strip_sorts o - Term_Subst.map_atypsT (fn U => + Term.map_atyps (fn U => if member (op =) atyps U then #typ_operation ucontext {strip_sorts = false} U else raise Same.SAME);