expand_split_asm -> split_split_asm

--- a/src/HOL/Product_Type.ML	Wed Nov 29 17:23:27 2000 +0100
+++ b/src/HOL/Product_Type.ML	Wed Nov 29 17:24:20 2000 +0100
@@ -275,7 +275,7 @@
 Goal "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))";
 by (stac split_split 1);
 by (Simp_tac 1);
-qed "expand_split_asm";
+qed "split_split_asm";
 
 (** split used as a logical connective or set former **)