Removed structure Prod_Syntax.

--- a/src/HOL/Lfp.ML	Tue Jun 30 20:42:47 1998 +0200
+++ b/src/HOL/Lfp.ML	Tue Jun 30 20:43:36 1998 +0200
@@ -51,10 +51,8 @@
             rtac (CollectI RS subsetI), rtac indhyp, atac]);
 qed "induct";
 
-bind_thm
-  ("induct2",
-   Prod_Syntax.split_rule
-     (read_instantiate [("a","(a,b)")] induct));
+bind_thm ("induct2",
+  split_rule (read_instantiate [("a","(a,b)")] induct));
 
 
 (** Definition forms of lfp_Tarski and induct, to control unfolding **)

--- a/src/HOL/Trancl.ML	Tue Jun 30 20:42:47 1998 +0200
+++ b/src/HOL/Trancl.ML	Tue Jun 30 20:43:36 1998 +0200
@@ -71,10 +71,8 @@
 by (blast_tac (claset() addIs prems) 1);
 qed "rtrancl_induct";
 
-bind_thm
-  ("rtrancl_induct2",
-   Prod_Syntax.split_rule
-     (read_instantiate [("a","(ax,ay)"), ("b","(bx,by)")] rtrancl_induct));
+bind_thm ("rtrancl_induct2", split_rule
+  (read_instantiate [("a","(ax,ay)"), ("b","(bx,by)")] rtrancl_induct));
 
 (*transitivity of transitive closure!! -- by induction.*)
 Goalw [trans_def] "trans(r^*)";