src/HOL/indrule.ML
changeset 1746 f0c6aabc6c02
parent 1728 01beef6262aa
child 1861 505b104f675a
--- a/src/HOL/indrule.ML	Wed May 15 13:51:15 1996 +0200
+++ b/src/HOL/indrule.ML	Fri May 17 12:23:44 1996 +0200
@@ -102,9 +102,9 @@
   Splits cartesian products in elem_type, however nested*)
 
 (*The components of the element type, several if it is a product*)
-val elem_factors = Ind_Syntax.factors elem_type;
+val elem_factors = Prod_Syntax.factors elem_type;
 val elem_frees = mk_frees "za" elem_factors;
-val elem_tuple = Ind_Syntax.mk_tuple elem_type elem_frees;
+val elem_tuple = Prod_Syntax.mk_tuple elem_type elem_frees;
 
 (*Given a recursive set, return the "split" predicate
   and a conclusion for the simultaneous induction rule*)
@@ -117,7 +117,7 @@
           (elem_frees, 
            Ind_Syntax.imp $ (Ind_Syntax.mk_mem (elem_tuple, rec_tm))
                 $ (list_comb (pfree, elem_frees)))
-  in  (Ind_Syntax.ap_split elem_type Ind_Syntax.boolT pfree, 
+  in  (Prod_Syntax.ap_split elem_type Ind_Syntax.boolT pfree, 
        qconcl)  
   end;
 
@@ -214,14 +214,14 @@
 in
   struct
   val induct = standard 
-                  (Ind_Syntax.split_rule_var
+                  (Prod_Syntax.split_rule_var
 		    (Var((pred_name,2), elem_type --> Ind_Syntax.boolT),
 		     induct0));
 
   (*Just "True" unless there's true mutual recursion.  This saves storage.*)
   val mutual_induct = 
       if length Intr_elim.rec_names > 1
-      then Ind_Syntax.remove_split mutual_induct_split
+      then Prod_Syntax.remove_split mutual_induct_split
       else TrueI;
   end
 end;