# HG changeset patch
# User wenzelm
# Date 1703005405 -3600
# Node ID cf8ccfec5059f1a32d0af928b051af312d040914
# Parent  c9f253e9125731dfc094bf11fc962c132f5bdf3c
more normalization: re-use Thm.solve_constraints as important checkpoint for results, notably Global_Theory.name_thm;

diff -r c9f253e91257 -r cf8ccfec5059 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Dec 19 17:54:55 2023 +0100
+++ b/src/Pure/thm.ML	Tue Dec 19 18:03:25 2023 +0100
@@ -1008,24 +1008,25 @@
 in
 
 fun solve_constraints (thm as Thm (der, args)) =
-      let
-        val {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop} = args;
+  let
+    val {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop} = args;
+
+    val bad_thys = map_filter (bad_constraint_theory cert) constraints;
+    val _ =
+      if null bad_thys then ()
+      else
+        raise THEORY ("solve_constraints: bad theories for theorem\n" ^
+          Syntax.string_of_term_global (hd bad_thys) (prop_of thm), bad_thys);
 
-        val bad_thys = map_filter (bad_constraint_theory cert) constraints;
-        val _ =
-          if null bad_thys then ()
-          else
-            raise THEORY ("solve_constraints: bad theories for theorem\n" ^
-              Syntax.string_of_term_global (hd bad_thys) (prop_of thm), bad_thys);
-
-        val Deriv {promises, body = PBody {oracles, thms, zboxes, zproof, proof}} = der;
-        val (oracles', thms') = (oracles, thms)
-          |> fold (fold union_digest o constraint_digest) constraints;
-      in
-        Thm (make_deriv promises oracles' thms' zboxes zproof proof,
-          {constraints = [], cert = cert, tags = tags, maxidx = maxidx,
-            shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop})
-      end;
+    val Deriv {promises, body = PBody {oracles, thms, zboxes, zproof, proof}} = der;
+    val (oracles', thms') = (oracles, thms)
+      |> fold (fold union_digest o constraint_digest) constraints;
+    val zproof' = ZTerm.beta_norm_prooft zproof;
+  in
+    Thm (make_deriv promises oracles' thms' zboxes zproof' proof,
+      {constraints = [], cert = cert, tags = tags, maxidx = maxidx,
+        shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop})
+  end;
 
 end;