# HG changeset patch # User wenzelm # Date 1701864994 -3600 # Node ID feb94ac5df414fc757e8a8573df3dbd8a1622155 # Parent a9c55fef42b0d854575dec3f7cc5aea25c953d53 more accurate treatment of term variables after instantiation of type variables; diff -r a9c55fef42b0 -r feb94ac5df41 src/Pure/term_items.ML --- a/src/Pure/term_items.ML Wed Dec 06 13:04:07 2023 +0100 +++ b/src/Pure/term_items.ML Wed Dec 06 13:16:34 2023 +0100 @@ -32,6 +32,7 @@ val make1: key * 'a -> 'a table val make2: key * 'a -> key * 'a -> 'a table val make3: key * 'a -> key * 'a -> key * 'a -> 'a table + val make_strict: (key * 'a) list -> 'a table type set = int table val add_set: key -> set -> set val make_set: key list -> set @@ -81,6 +82,8 @@ fun make2 e1 e2 = build (add e1 #> add e2); fun make3 e1 e2 e3 = build (add e1 #> add e2 #> add e3); +fun make_strict es = Table (Table.make es); + (* set with order of addition *) diff -r a9c55fef42b0 -r feb94ac5df41 src/Pure/zterm.ML --- a/src/Pure/zterm.ML Wed Dec 06 13:04:07 2023 +0100 +++ b/src/Pure/zterm.ML Wed Dec 06 13:16:34 2023 +0100 @@ -236,21 +236,33 @@ fun map_insts_same typ term (instT, inst) = let val changed = Unsynchronized.ref false; + fun apply f x = + (case Same.catch f x of + NONE => NONE + | some => (changed := true; some)); + val instT' = (instT, instT) |-> ZTVars.fold (fn (v, T) => - (case Same.catch typ T of - SOME U => (changed := true; ZTVars.update (v, U)) - | NONE => I)); + (case apply typ T of + NONE => I + | SOME T' => ZTVars.update (v, T'))); + + val vars' = + (inst, ZVars.empty) |-> ZVars.fold (fn ((v, T), _) => + (case apply typ T of + NONE => I + | SOME T' => ZVars.add ((v, T), (v, T')))); + val inst' = - if ! changed then + if ZVars.is_empty vars' then + (inst, inst) |-> ZVars.fold (fn (v, t) => + (case apply term t of + NONE => I + | SOME t' => ZVars.update (v, t'))) + else ZVars.dest inst - |> map (fn ((x, T), t) => ((x, Same.commit typ T), Same.commit term t)) - |> ZVars.make - else - (inst, inst) |-> ZVars.fold (fn (v, t) => - (case Same.catch term t of - SOME u => (changed := true; ZVars.update (v, u)) - | NONE => I)); + |> map (fn (v, t) => (the_default v (ZVars.lookup vars' v), the_default t (apply term t))) + |> ZVars.make_strict; in if ! changed then (instT', inst') else raise Same.SAME end; fun map_proof_same typ term =