author | wenzelm |
Thu, 11 Jan 2024 12:00:02 +0100 | |
changeset 79473 | e1b2595d678a |
parent 79472 | 27279c76a068 |
child 79474 | c39aed404ffc |
src/Pure/zterm.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/zterm.ML Wed Jan 10 22:25:34 2024 +0100 +++ b/src/Pure/zterm.ML Thu Jan 11 12:00:02 2024 +0100 @@ -830,7 +830,7 @@ let val {zterm, ...} = zterm_cache thy; - val present_set = Types.build (fold Types.add_atyps hyps #> Types.add_atyps concl); + val present_set = Types.build (Types.add_atyps concl #> fold Types.add_atyps hyps); val ucontext as {constraints, outer_constraints, ...} = Logic.unconstrain_context [] present_set;