use split_tupled_all;

--- a/src/HOL/Real/HahnBanach/Subspace.thy	Sun Jul 16 20:57:34 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Sun Jul 16 20:59:06 2000 +0200
@@ -420,7 +420,7 @@
   "[| is_vectorspace E; is_subspace H E; t:H; x0 ~: H; x0:E;
   x0 ~= 00 |] 
   ==> (SOME (y, a). t = y + a (*) x0 & y : H) = (t, (#0::real))"
-proof (rule, unfold split_paired_all)
+proof (rule, unfold split_tupled_all)
   assume "is_vectorspace E" "is_subspace H E" "t:H" "x0 ~: H" "x0:E"
     "x0 ~= 00"
   have h: "is_vectorspace H" ..
@@ -459,7 +459,7 @@
     show "xa = ya" 
     proof -
       show "fst xa = fst ya & snd xa = snd ya ==> xa = ya" 
-        by (rule Pair_fst_snd_eq [RS iffD2])
+        by (simp add: Pair_fst_snd_eq)
       have x: "x = fst xa + snd xa (*) x0 & fst xa : H" 
         by (force!)
       have y: "x = fst ya + snd ya (*) x0 & fst ya : H"