# HG changeset patch
# User wenzelm
# Date 1702995424 -3600
# Node ID 0b1fd4445329574ded64e94408b24c2f2e848882
# Parent  fed9791928bf41b411269e2261e1171138e24f71
more normalization;

diff -r fed9791928bf -r 0b1fd4445329 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Tue Dec 19 14:41:28 2023 +0100
+++ b/src/Pure/zterm.ML	Tue Dec 19 15:17:04 2023 +0100
@@ -792,8 +792,8 @@
     val hyps' = map zterm hyps;
     val concl' = zterm concl;
 
-    val prop' = close_prop hyps' concl';
-    val prf' = close_proof hyps' prf;
+    val prop' = beta_norm_term (close_prop hyps' concl');
+    val prf' = beta_norm_prooft (close_proof hyps' prf);
 
     val i = serial ();
     val zboxes' = add_zboxes (i, (prop', Future.value prf')) zboxes;