diff -r ec6dfd9ce573 -r 150f831ce4a3 src/HOL/ex/Unification.thy
--- a/src/HOL/ex/Unification.thy	Tue Sep 28 09:43:13 2010 +0200
+++ b/src/HOL/ex/Unification.thy	Tue Sep 28 09:54:07 2010 +0200
@@ -158,6 +158,7 @@
                                          Some \<sigma> \<Rightarrow> Some (\<theta> \<bullet> \<sigma>)))"
   by pat_completeness auto
 
+declare unify.psimps[simp]
 
 subsection {* Partial correctness *}
 
@@ -533,4 +534,6 @@
   qed
 qed
 
+declare unify.psimps[simp del]
+
 end