# HG changeset patch
# User krauss
# Date 1240300411 -7200
# Node ID bd4f255837e51acbb023419bc8b88af30667d53d
# Parent  7ccf4a3d764cac5334499c7ba3ab7b3a4ab1e227
tuned proof

diff -r 7ccf4a3d764c -r bd4f255837e5 src/HOL/ex/Unification.thy
--- a/src/HOL/ex/Unification.thy	Tue Apr 21 09:53:27 2009 +0200
+++ b/src/HOL/ex/Unification.thy	Tue Apr 21 09:53:31 2009 +0200
@@ -277,7 +277,7 @@
     by (induct t) simp_all
 qed
 
-lemma var_same: "(t = Var v) = ([(v, t)] =\<^sub>s [])"
+lemma var_same: "([(v, t)] =\<^sub>s []) = (t = Var v)"
 proof
   assume t_v: "t = Var v"
   thus "[(v, t)] =\<^sub>s []"
@@ -307,7 +307,7 @@
   proof cases
     assume "v = x"
     thus ?thesis
-      by (simp add:var_same[symmetric])
+      by (simp add:var_same)
   next
     assume neq: "v \<noteq> x"
     have "elim [(v, Var x)] v"
@@ -328,13 +328,13 @@
     by auto
 
   from nonocc have "\<not> [(v,M)] =\<^sub>s []"
-    by (simp add:var_same[symmetric])
+    by (simp add:var_same)
   with ih1 have "elim [(v, M)] v" by blast
   hence "v \<notin> vars_of (Var v \<triangleleft> [(v,M)])" ..
   hence not_in_M: "v \<notin> vars_of M" by simp
 
   from nonocc have "\<not> [(v,N)] =\<^sub>s []"
-    by (simp add:var_same[symmetric])
+    by (simp add:var_same)
   with ih2 have "elim [(v, N)] v" by blast
   hence "v \<notin> vars_of (Var v \<triangleleft> [(v,N)])" ..
   hence not_in_N: "v \<notin> vars_of N" by simp