# HG changeset patch
# User paulson
# Date 905530194 -7200
# Node ID e9430ed7e8d6986dc66489a3a70b2330cddfcdd5
# Parent  2fc3f4450fe8af2cfdcd457aa0409d7ae96681a7
Extra steps at end to make it run faster

diff -r 2fc3f4450fe8 -r e9430ed7e8d6 src/HOL/UNITY/Lift.ML
--- a/src/HOL/UNITY/Lift.ML	Fri Sep 11 17:20:58 1998 +0200
+++ b/src/HOL/UNITY/Lift.ML	Fri Sep 11 18:09:54 1998 +0200
@@ -457,11 +457,12 @@
 by (rtac subset_imp_LeadsTo 1);
 by (rtac id_in_Acts 2);
 by (Clarify_tac 1);
-	(*stops simplification from looping*)
-by (Full_simp_tac 1);
+(*The case split is not essential but makes Blast_tac much faster.
+  Must also be careful to prevent simplification from looping*)
+by (case_tac "open x" 1);
+by (ALLGOALS (rotate_tac ~1));
+by (ALLGOALS Asm_full_simp_tac);
 by (Blast_tac 1);
 qed "lift_1";
 
 Close_locale;
-
-