Moved most of the Prod_Syntax - stuff to HOLogic.

--- a/src/HOL/Prod.ML	Tue Jun 30 20:40:29 1998 +0200
+++ b/src/HOL/Prod.ML	Tue Jun 30 20:41:41 1998 +0200
@@ -428,59 +428,39 @@
 Addsimps [unit_abs_eta_conv];
 
 
-structure Prod_Syntax =		(* FIXME eliminate (use HOLogic instead!) *)
-struct
-
-val unitT = Type("unit",[]);
-
-fun mk_prod (T1,T2) = Type("*", [T1,T2]);
+(*Attempts to remove occurrences of split, and pair-valued parameters*)
+val remove_split = rewrite_rule [split RS eq_reflection] o  
+                   rule_by_tactic (TRYALL split_all_tac);
 
-(*Maps the type T1*...*Tn to [T1,...,Tn], however nested*)
-fun factors (Type("*", [T1,T2])) = factors T1 @ factors T2
-  | factors T                    = [T];
-
-(*Make a correctly typed ordered pair*)
-fun mk_Pair (t1,t2) = 
-  let val T1 = fastype_of t1
-      and T2 = fastype_of t2
-  in  Const("Pair", [T1, T2] ---> mk_prod(T1,T2)) $ t1 $ t2  end;
-   
-fun split_const(Ta,Tb,Tc) = 
-    Const("split", [[Ta,Tb]--->Tc, mk_prod(Ta,Tb)] ---> Tc);
+local
 
 (*In ap_split S T u, term u expects separate arguments for the factors of S,
   with result type T.  The call creates a new term expecting one argument
   of type S.*)
-fun ap_split (Type("*", [T1,T2])) T3 u = 
-      split_const(T1,T2,T3) $ 
+fun ap_split (Type ("*", [T1, T2])) T3 u = 
+      HOLogic.split_const (T1, T2, T3) $ 
       Abs("v", T1, 
           ap_split T2 T3
-             ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $ 
+             ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $ 
               Bound 0))
   | ap_split T T3 u = u;
 
-(*Makes a nested tuple from a list, following the product type structure*)
-fun mk_tuple (Type("*", [T1,T2])) tms = 
-        mk_Pair (mk_tuple T1 tms, 
-                 mk_tuple T2 (drop (length (factors T1), tms)))
-  | mk_tuple T (t::_) = t;
-
-(*Attempts to remove occurrences of split, and pair-valued parameters*)
-val remove_split = rewrite_rule [split RS eq_reflection]  o  
-                   rule_by_tactic (TRYALL split_all_tac);
+(*Curries any Var of function type in the rule*)
+fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2])), rl) =
+      let val T' = HOLogic.prodT_factors T1 ---> T2
+          val newt = ap_split T1 T2 (Var (v, T'))
+          val cterm = Thm.cterm_of (#sign (rep_thm rl))
+      in
+          instantiate ([], [(cterm t, cterm newt)]) rl
+      end
+  | split_rule_var' (t, rl) = rl;
 
-(*Uncurries any Var of function type in the rule*)
-fun split_rule_var (t as Var(v, Type("fun",[T1,T2])), rl) =
-      let val T' = factors T1 ---> T2
-          val newt = ap_split T1 T2 (Var(v,T'))
-          val cterm = Thm.cterm_of (#sign(rep_thm rl))
-      in
-          remove_split (instantiate ([], [(cterm t, cterm newt)]) rl)
-      end
-  | split_rule_var (t,rl) = rl;
+in
 
-(*Uncurries ALL function variables occurring in a rule's conclusion*)
-fun split_rule rl = foldr split_rule_var (term_vars (concl_of rl), rl)
+val split_rule_var = standard o remove_split o split_rule_var';
+
+(*Curries ALL function variables occurring in a rule's conclusion*)
+fun split_rule rl = remove_split (foldr split_rule_var' (term_vars (concl_of rl), rl))
                     |> standard;
 
 end;

--- a/src/HOL/hologic.ML	Tue Jun 30 20:40:29 1998 +0200
+++ b/src/HOL/hologic.ML	Tue Jun 30 20:41:41 1998 +0200
@@ -47,6 +47,9 @@
   val dest_prod: term -> term * term
   val mk_fst: term -> term
   val mk_snd: term -> term
+  val prodT_factors: typ -> typ list
+  val split_const: typ * typ * typ -> term
+  val mk_tuple: typ -> term list -> term
 end;
 
 
@@ -182,5 +185,17 @@
     Const ("snd", pT --> snd (dest_prodT pT)) $ p
   end;
 
+(*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
+fun prodT_factors (Type ("*", [T1, T2])) = prodT_factors T1 @ prodT_factors T2
+  | prodT_factors T = [T];
+
+fun split_const (Ta, Tb, Tc) = 
+    Const ("split", [[Ta, Tb] ---> Tc, mk_prodT (Ta, Tb)] ---> Tc);
+
+(*Makes a nested tuple from a list, following the product type structure*)
+fun mk_tuple (Type ("*", [T1, T2])) tms = 
+        mk_prod (mk_tuple T1 tms, 
+                 mk_tuple T2 (drop (length (prodT_factors T1), tms)))
+  | mk_tuple T (t::_) = t;
 
 end;