clarified order: follow Thm.fold_terms;
authorwenzelm
Thu, 11 Jan 2024 12:00:02 +0100
changeset 79473 e1b2595d678a
parent 79472 27279c76a068
child 79474 c39aed404ffc
clarified order: follow Thm.fold_terms;
src/Pure/zterm.ML
--- 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;