more normalization;

--- 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;