# HG changeset patch
# User desharna
# Date 1656534788 -7200
# Node ID b8bd0189757857bde3a9d7f0f7618d81447ccb1e
# Parent  aaa22adef0399943944278419b66e7cf6dcdb56a
tuned proof

diff -r aaa22adef039 -r b8bd01897578 src/HOL/ex/Unification.thy
--- a/src/HOL/ex/Unification.thy	Wed Jun 29 20:41:29 2022 +0200
+++ b/src/HOL/ex/Unification.thy	Wed Jun 29 22:33:08 2022 +0200
@@ -686,7 +686,7 @@
 
   from "7.hyps"(2) have "fst ` set \<theta>\<^sub>2 \<subseteq> vars_of (N \<lhd> \<theta>\<^sub>1) \<union> vars_of (N' \<lhd> \<theta>\<^sub>1)"
     using \<open>unify M M' = Some \<theta>\<^sub>1\<close> \<open>unify (N \<lhd> \<theta>\<^sub>1) (N' \<lhd> \<theta>\<^sub>1) = Some \<theta>\<^sub>2\<close> by simp
-  hence dom_\<theta>\<^sub>2': "fst ` set \<theta>\<^sub>2 \<subseteq> vars_of N \<union> vars_of N' \<union> range_vars \<theta>\<^sub>1"
+  hence dom_\<theta>\<^sub>2: "fst ` set \<theta>\<^sub>2 \<subseteq> vars_of N \<union> vars_of N' \<union> range_vars \<theta>\<^sub>1"
     using vars_of_subst_subset[of _ \<theta>\<^sub>1] by auto
 
   have "fst ` set \<sigma> = fst ` set (\<theta>\<^sub>1 \<lozenge> \<theta>\<^sub>2)"
@@ -696,7 +696,7 @@
   also have "... \<subseteq> vars_of M \<union> vars_of M' \<union> fst ` set \<theta>\<^sub>2"
     using dom_\<theta>\<^sub>1 by (auto simp: dom_map_of_conv_image_fst)
   also have "... \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of N \<union> vars_of N' \<union> range_vars \<theta>\<^sub>1"
-    using dom_\<theta>\<^sub>2' by (auto simp: dom_map_of_conv_image_fst)
+    using dom_\<theta>\<^sub>2 by (auto simp: dom_map_of_conv_image_fst)
   also have "... \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of N \<union> vars_of N'"
     using unify_gives_minimal_range[OF \<open>unify M M' = Some \<theta>\<^sub>1\<close>] by auto
   finally show ?case