--- 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)