# HG changeset patch
# User wenzelm
# Date 1325249527 -3600
# Node ID badf0572e1bcd96d8a0a540d7da2130e574cbb98
# Parent  014aed021a5eca2ab3c30cbb9bd1e56c14d12003
simplified proof;

diff -r 014aed021a5e -r badf0572e1bc src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri Dec 30 12:54:55 2011 +0100
+++ b/src/HOL/Tools/record.ML	Fri Dec 30 13:52:07 2011 +0100
@@ -2187,13 +2187,13 @@
           rtac split_meta 1));
 
     val split_ex = timeit_msg ctxt "record split_ex proof:" (fn () =>
-      let
-        val ss = HOL_basic_ss addsimps @{thms not_ex [symmetric] Not_eq_iff};
-        val P_nm = fst (dest_Free P);
-        val not_P = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0)));
-        val so' = named_cterm_instantiate ([(P_nm, not_P)]) split_object;
-        val so'' = simplify ss so';
-      in Skip_Proof.prove_global defs_thy [] [] split_ex_prop (fn _ => resolve_tac [so''] 1) end);
+      Skip_Proof.prove_global defs_thy [] [] split_ex_prop
+        (fn _ =>
+          simp_tac
+            (HOL_basic_ss addsimps
+              (@{lemma "EX x. P x == ~ (ALL x. ~ P x)" by simp} ::
+                @{thms not_not Not_eq_iff})) 1 THEN
+          rtac split_object 1));
 
     fun equality_tac thms =
       let