1.1 --- a/src/HOL/ex/Unification.thy	Tue Sep 28 09:43:13 2010 +0200
     1.2 +++ b/src/HOL/ex/Unification.thy	Tue Sep 28 09:54:07 2010 +0200
     1.3 @@ -158,6 +158,7 @@
     1.4                                           Some \<sigma> \<Rightarrow> Some (\<theta> \<bullet> \<sigma>)))"
     1.5    by pat_completeness auto
     1.6  
     1.7 +declare unify.psimps[simp]
     1.8  
     1.9  subsection {* Partial correctness *}
    1.10  
    1.11 @@ -533,4 +534,6 @@
    1.12    qed
    1.13  qed
    1.14  
    1.15 +declare unify.psimps[simp del]
    1.16 +
    1.17  end