# HG changeset patch
# User haftmann
# Date 1318539379 -7200
# Node ID ba618e9288b859f2d6c9e1b0c7468fb05d04aa50
# Parent  6e422d180de80a9cdd5012fbac9885ce39e699e0
tuned

diff -r 6e422d180de8 -r ba618e9288b8 src/HOL/UNITY/UNITY_tactics.ML
--- a/src/HOL/UNITY/UNITY_tactics.ML	Thu Oct 13 22:56:19 2011 +0200
+++ b/src/HOL/UNITY/UNITY_tactics.ML	Thu Oct 13 22:56:19 2011 +0200
@@ -46,7 +46,7 @@
       ORELSE res_inst_tac ctxt
         [(("act", 0), sact)] @{thm transientI} 2,
          (*simplify the command's domain*)
-      simp_tac (simpset_of ctxt addsimps [@{thm Domain_def}]) 3,
+      simp_tac (simpset_of ctxt addsimps @{thms Domain_def}) 3,
       constrains_tac ctxt 1,
       ALLGOALS (clarify_tac ctxt),
       ALLGOALS (asm_lr_simp_tac (simpset_of ctxt))]);