# HG changeset patch
# User paulson
# Date 1262516602 0
# Node ID 43bf58fdbacea7affe8622d6878e7cd67e4db320
# Parent  156c42518cfcca3b86ef54cbdf5c818e6ffbe48d# Parent  86a985e9b4df0f4927b8b49ae53376e4fd0cb124
merged

diff -r 156c42518cfc -r 43bf58fdbace src/HOL/UNITY/UNITY_tactics.ML
--- a/src/HOL/UNITY/UNITY_tactics.ML	Sun Jan 03 10:01:23 2010 +0100
+++ b/src/HOL/UNITY/UNITY_tactics.ML	Sun Jan 03 11:03:22 2010 +0000
@@ -29,7 +29,7 @@
               full_simp_tac ss 1,
               REPEAT (FIRSTGOAL (etac disjE)),
               ALLGOALS (clarify_tac cs),
-              ALLGOALS (asm_lr_simp_tac ss)]) i;
+              ALLGOALS (asm_full_simp_tac ss)]) i;
 
 (*proves "ensures/leadsTo" properties when the program is specified*)
 fun ensures_tac(cs,ss) sact =