diff -r 5a4f382455ce -r a70a5bc5e315 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Wed May 08 17:59:21 1996 +0200
+++ b/src/ZF/ind_syntax.ML	Wed May 08 18:01:54 1996 +0200
@@ -17,13 +17,8 @@
 val iT = Type("i",[])
 and oT = Type("o",[]);
 
-(*Given u expecting arguments of types [T1,...,Tn], create term of 
-  type T1*...*Tn => i using split*)
-fun ap_split split u [ ]   = Abs("null", iT, u)
-  | ap_split split u [_]   = u
-  | ap_split split u [_,_] = split $ u
-  | ap_split split u (T::Ts) = 
-      split $ (Abs("v", T, ap_split split (u $ Bound(length Ts - 2)) Ts));
+
+(** Logical constants **)
 
 val conj = Const("op &", [oT,oT]--->oT)
 and disj = Const("op |", [oT,oT]--->oT)