# HG changeset patch
# User wenzelm
# Date 1702845284 -3600
# Node ID 899f37f6d2183070ae04b0eb2b0b7317d307635c
# Parent  b14b289caaf605a29ab27d2fba05dcb858787266
proper beta_norm after instantiation (amending 90c5aadcc4b2);

diff -r b14b289caaf6 -r 899f37f6d218 src/Pure/General/same.ML
--- a/src/Pure/General/same.ML	Sun Dec 17 21:30:21 2023 +0100
+++ b/src/Pure/General/same.ML	Sun Dec 17 21:34:44 2023 +0100
@@ -14,6 +14,7 @@
   val commit: 'a operation -> 'a -> 'a
   val commit_id: 'a operation -> 'a -> 'a * bool
   val catch: ('a, 'b) function -> 'a -> 'b option
+  val compose: 'a operation -> 'a operation -> 'a operation
   val function: ('a -> 'b option) -> ('a, 'b) function
   val map: 'a operation -> 'a list operation
   val map_option: ('a, 'b) function -> ('a option, 'b option) function
@@ -33,6 +34,11 @@
 
 fun catch f x = SOME (f x) handle SAME => NONE;
 
+fun compose g f x =
+  (case catch f x of
+    NONE => g x
+  | SOME y => commit g y);
+
 fun function f x =
   (case f x of
     NONE => raise SAME
diff -r b14b289caaf6 -r 899f37f6d218 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Sun Dec 17 21:30:21 2023 +0100
+++ b/src/Pure/zterm.ML	Sun Dec 17 21:34:44 2023 +0100
@@ -617,7 +617,9 @@
           val inst_term =
             ZVars.build (visible |> (fold o Term.fold_aterms) (fn Var v => add_var v | _ => I))
             |> instantiate_term_same inst_typ;
-        in Same.commit (map_proof_same inst_typ inst_term) prf end
+
+          val norm_term = Same.compose beta_norm_same inst_term;
+        in Same.commit (map_proof_same inst_typ norm_term) prf end
   end;
 
 fun norm_cache thy =