# HG changeset patch
# User berghofe
# Date 899232216 -7200
# Node ID 48e70d9fe05f919644604ab4e5b9b7962e7a6397
# Parent  6c4a7ad6ebc782b3a9fe4498544b4ccce7056352
Removed structure Prod_Syntax.

diff -r 6c4a7ad6ebc7 -r 48e70d9fe05f src/HOL/Lfp.ML
--- 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 **)
diff -r 6c4a7ad6ebc7 -r 48e70d9fe05f src/HOL/Trancl.ML
--- 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^*)";