# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1223149828 14400
# Node ID b85e6ba5661867222b6f41ebf6f40f63cf78bc9e
# Parent  3c0feecd057da86ee2c2bc1a0381a90e1b85ce57
Merge CDisjoint and TDisjoint

diff -r 3c0feecd057d -r b85e6ba56618 lib/basis.urs
--- a/lib/basis.urs	Thu Sep 18 15:01:01 2008 -0400
+++ b/lib/basis.urs	Sat Oct 04 15:50:28 2008 -0400
@@ -189,7 +189,7 @@
         -> transaction t2
 
 val query : tables ::: {{Type}} -> exps ::: {Type} -> tables ~ exps
-        -> state ::: Type
+        => state ::: Type
         -> sql_query tables exps
         -> ($(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)
                 -> state
@@ -210,7 +210,7 @@
         -> dml
 
 val update : changed :: {Type} -> unchanged ::: {Type} -> changed ~ unchanged
-        -> $(fold (fn nm (t :: Type) acc => [nm] ~ acc =>
+        => $(fold (fn nm (t :: Type) acc => [nm] ~ acc =>
                 [nm = sql_exp [T = changed ++ unchanged] [] [] t] ++ acc) [] changed)
         -> sql_table (changed ++ unchanged)
         -> sql_exp [T = changed ++ unchanged] [] [] bool
@@ -235,22 +235,22 @@
 con xml :: {Unit} -> {Type} -> {Type} -> Type
 val cdata : ctx ::: {Unit} -> use ::: {Type} -> string -> xml ctx use []
 val tag : attrsGiven ::: {Type} -> attrsAbsent ::: {Type} -> attrsGiven ~ attrsAbsent
-        -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit}
+        => ctxOuter ::: {Unit} -> ctxInner ::: {Unit}
         -> useOuter ::: {Type} -> useInner ::: {Type} -> useOuter ~ useInner
-        -> bindOuter ::: {Type} -> bindInner ::: {Type} -> bindOuter ~ bindInner
-        -> $attrsGiven
+        => bindOuter ::: {Type} -> bindInner ::: {Type} -> bindOuter ~ bindInner
+        => $attrsGiven
         -> tag (attrsGiven ++ attrsAbsent) ctxOuter ctxInner useOuter bindOuter
         -> xml ctxInner useInner bindInner
         -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner)
 val join : ctx ::: {Unit} 
         -> use1 ::: {Type} -> bind1 ::: {Type} -> bind2 ::: {Type}
-        -> use1 ~ bind1 -> bind1 ~ bind2
-        -> xml ctx use1 bind1
+        -> use1 ~ bind1 => bind1 ~ bind2
+        => xml ctx use1 bind1
         -> xml ctx (use1 ++ bind1) bind2
         -> xml ctx use1 (bind1 ++ bind2)
 val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type} -> bind ::: {Type}
         -> use1 ~ use2
-        -> xml ctx use1 bind
+        => xml ctx use1 bind
         -> xml ctx (use1 ++ use2) bind
 
 con xhtml = xml [Html]
@@ -272,9 +272,9 @@
 val title : unit -> tag [] head [] [] []
 
 val body : unit -> tag [] html body [] []
-con bodyTag = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx -> unit
+con bodyTag = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx => unit
         -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] []
-con bodyTagStandalone = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx -> unit
+con bodyTagStandalone = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx => unit
         -> tag attrs ([Body] ++ ctx) [] [] []
 
 val br : bodyTagStandalone []
@@ -289,12 +289,12 @@
 
 val a : bodyTag [Link = transaction page]
 
-val lform : ctx ::: {Unit} -> [Body] ~ ctx -> bind ::: {Type}
+val lform : ctx ::: {Unit} -> [Body] ~ ctx => bind ::: {Type}
         -> xml form [] bind
         -> xml ([Body] ++ ctx) [] []
 con lformTag = fn ty :: Type => fn inner :: {Unit} => fn attrs :: {Type} =>
         ctx ::: {Unit} -> [LForm] ~ ctx
-        -> nm :: Name -> unit
+        => nm :: Name -> unit
         -> tag attrs ([LForm] ++ ctx) inner [] [nm = ty]
 val textbox : lformTag string [] [Value = string]
 val password : lformTag string [] []
@@ -311,7 +311,7 @@
 val loption : unit -> tag [Value = string] select [] [] []
 
 val submit : ctx ::: {Unit} -> [LForm] ~ ctx
-        -> use ::: {Type} -> unit
+        => use ::: {Type} -> unit
         -> tag [Action = $use -> transaction page] ([LForm] ++ ctx) ([LForm] ++ ctx) use []
 
 (*** Tables *)
diff -r 3c0feecd057d -r b85e6ba56618 lib/top.ur
--- a/lib/top.ur	Thu Sep 18 15:01:01 2008 -0400
+++ b/lib/top.ur	Sat Oct 04 15:50:28 2008 -0400
@@ -22,7 +22,7 @@
 
 fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type)
         (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
-                -> tf t -> tr rest -> tr ([nm = t] ++ rest))
+                => tf t -> tr rest -> tr ([nm = t] ++ rest))
         (i : tr []) =
         fold [fn r :: {Type} => $(mapTT tf r) -> tr r]
                 (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> tr rest) =>
@@ -32,7 +32,7 @@
 
 fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type)
         (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
-                -> tf t -> tr rest -> tr ([nm = t] ++ rest))
+                => tf t -> tr rest -> tr ([nm = t] ++ rest))
         (i : tr []) =
         fold [fn r :: {(Type * Type)} => $(mapT2T tf r) -> tr r]
                 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) (acc : _ -> tr rest) =>
@@ -42,7 +42,7 @@
 
 fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type)
         (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
-                -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+                => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
         (i : tr []) =
         fold [fn r :: {Type} => $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r]
                 (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> _ -> tr rest) =>
@@ -52,7 +52,7 @@
 
 fun foldT2R2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type)
         (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
-                -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+                => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
         (i : tr []) =
         fold [fn r :: {(Type * Type)} => $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r]
                 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) (acc : _ -> _ -> tr rest) =>
@@ -62,7 +62,7 @@
 
 fun foldTRX (tf :: Type -> Type) (ctx :: {Unit})
         (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
-                -> tf t -> xml ctx [] []) =
+                => tf t -> xml ctx [] []) =
         foldTR [tf] [fn _ => xml ctx [] []]
                 (fn (nm :: Name) (t :: Type) (rest :: {Type}) =>
                         [[nm] ~ rest] =>
@@ -71,7 +71,7 @@
 
 fun foldT2RX (tf :: (Type * Type) -> Type) (ctx :: {Unit})
         (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
-                -> tf t -> xml ctx [] []) =
+                => tf t -> xml ctx [] []) =
         foldT2R [tf] [fn _ => xml ctx [] []]
                 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) =>
                         [[nm] ~ rest] =>
@@ -80,7 +80,7 @@
 
 fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit})
         (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
-                -> tf1 t -> tf2 t -> xml ctx [] []) =
+                => tf1 t -> tf2 t -> xml ctx [] []) =
         foldTR2 [tf1] [tf2] [fn _ => xml ctx [] []]
                 (fn (nm :: Name) (t :: Type) (rest :: {Type}) =>
                         [[nm] ~ rest] =>
@@ -89,7 +89,7 @@
 
 fun foldT2RX2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) (ctx :: {Unit})
         (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
-                -> tf1 t -> tf2 t -> xml ctx [] []) =
+                => tf1 t -> tf2 t -> xml ctx [] []) =
         foldT2R2 [tf1] [tf2] [fn _ => xml ctx [] []]
                 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) =>
                         [[nm] ~ rest] =>
diff -r 3c0feecd057d -r b85e6ba56618 lib/top.urs
--- a/lib/top.urs	Thu Sep 18 15:01:01 2008 -0400
+++ b/lib/top.urs	Sat Oct 04 15:50:28 2008 -0400
@@ -22,52 +22,52 @@
 
 val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type)
         -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
-                -> tf t -> tr rest -> tr ([nm = t] ++ rest))
+                => tf t -> tr rest -> tr ([nm = t] ++ rest))
         -> tr [] -> r :: {Type} -> $(mapTT tf r) -> tr r
 
 val foldT2R : tf :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type)
         -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
-                -> tf t -> tr rest -> tr ([nm = t] ++ rest))
+                => tf t -> tr rest -> tr ([nm = t] ++ rest))
         -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf r) -> tr r
 
 val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> tr :: ({Type} -> Type)
         -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
-                -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+                => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
         -> tr [] -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r
 
 val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
         -> tr :: ({(Type * Type)} -> Type)
         -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
-                -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+                => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
         -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r
 
 val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit}
         -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
-                -> tf t -> xml ctx [] [])
+                => tf t -> xml ctx [] [])
         -> r :: {Type} -> $(mapTT tf r) -> xml ctx [] []
 
 val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit}
         -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
-                -> tf t -> xml ctx [] [])
+                => tf t -> xml ctx [] [])
         -> r :: {(Type * Type)} -> $(mapT2T tf r) -> xml ctx [] []
 
 val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit}
         -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
-                -> tf1 t -> tf2 t -> xml ctx [] [])
+                => tf1 t -> tf2 t -> xml ctx [] [])
         -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> xml ctx [] []
 
 val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) -> ctx :: {Unit}
         -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
-                -> tf1 t -> tf2 t -> xml ctx [] [])
+                => tf1 t -> tf2 t -> xml ctx [] [])
         -> r :: {(Type * Type)} -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> xml ctx [] []
 
 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
         -> sql_query tables exps -> tables ~ exps
-        -> ($(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)
+        => ($(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)
                 -> xml ctx [] [])
         -> transaction (xml ctx [] [])
 
 val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type} -> sql_query tables exps
         -> tables ~ exps
-        -> transaction
+        => transaction
                 (option $(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables))
diff -r 3c0feecd057d -r b85e6ba56618 src/disjoint.sml
--- a/src/disjoint.sml	Thu Sep 18 15:01:01 2008 -0400
+++ b/src/disjoint.sml	Sat Oct 04 15:50:28 2008 -0400
@@ -315,8 +315,7 @@
             end
     in
         case c of
-            CDisjoint cs => doDisj cs
-          | TDisjoint (Instantiate, c1, c2, c) => doDisj (c1, c2, c)
+            CDisjoint (Instantiate, c1, c2, c) => doDisj (c1, c2, c)
           | _ => (cAll, [])
     end
 
diff -r 3c0feecd057d -r b85e6ba56618 src/elab.sml
--- a/src/elab.sml	Thu Sep 18 15:01:01 2008 -0400
+++ b/src/elab.sml	Sat Oct 04 15:50:28 2008 -0400
@@ -53,7 +53,6 @@
 datatype con' =
          TFun of con * con
        | TCFun of explicitness * string * kind * con
-       | TDisjoint of auto_instantiate * con * con * con
        | TRecord of con
 
        | CRel of int
@@ -61,7 +60,7 @@
        | CModProj of int * string list * string
        | CApp of con * con
        | CAbs of string * kind * con
-       | CDisjoint of con * con * con
+       | CDisjoint of auto_instantiate * con * con * con
 
        | CName of string
 
diff -r 3c0feecd057d -r b85e6ba56618 src/elab_ops.sml
--- a/src/elab_ops.sml	Thu Sep 18 15:01:01 2008 -0400
+++ b/src/elab_ops.sml	Sat Oct 04 15:50:28 2008 -0400
@@ -146,7 +146,7 @@
                                    val c = (CApp (c, r), loc)
                                    fun unconstraint c =
                                        case hnormCon env c of
-                                           (CDisjoint (_, _, c), _) => unconstraint c
+                                           (CDisjoint (_, _, _, c), _) => unconstraint c
                                          | c => c
                                    val c = unconstraint c
 
diff -r 3c0feecd057d -r b85e6ba56618 src/elab_print.sml
--- a/src/elab_print.sml	Thu Sep 18 15:01:01 2008 -0400
+++ b/src/elab_print.sml	Sat Oct 04 15:50:28 2008 -0400
@@ -80,13 +80,13 @@
                                                 string "->",
                                                 space,
                                                 p_con (E.pushCRel env x k) c])
-      | TDisjoint (_, c1, c2, c3) => parenIf par (box [p_con env c1,
+      | CDisjoint (_, c1, c2, c3) => parenIf par (box [p_con env c1,
                                                        space,
                                                        string "~",
                                                        space,
                                                        p_con env c2,
                                                        space,
-                                                       string "->",
+                                                       string "=>",
                                                        space,
                                                        p_con env c3])
       | TRecord (CRecord (_, xcs), _) => box [string "{",
@@ -139,15 +139,6 @@
                                              string "=>",
                                              space,
                                              p_con (E.pushCRel env x k) c])
-      | CDisjoint (c1, c2, c3) => parenIf par (box [p_con env c1,
-                                                    space,
-                                                    string "~",
-                                                    space,
-                                                    p_con env c2,
-                                                    space,
-                                                    string "=>",
-                                                    space,
-                                                    p_con env c3])
 
       | CName s => box [string "#", string s]
 
diff -r 3c0feecd057d -r b85e6ba56618 src/elab_util.sml
--- a/src/elab_util.sml	Thu Sep 18 15:01:01 2008 -0400
+++ b/src/elab_util.sml	Sat Oct 04 15:50:28 2008 -0400
@@ -119,14 +119,14 @@
                          S.map2 (mfc (bind (ctx, Rel (x, k))) c,
                               fn c' =>
                                  (TCFun (e, x, k', c'), loc)))
-              | TDisjoint (ai, c1, c2, c3) =>
+              | CDisjoint (ai, c1, c2, c3) =>
                 S.bind2 (mfc ctx c1,
                       fn c1' =>
                          S.bind2 (mfc ctx c2,
                               fn c2' =>
                                  S.map2 (mfc ctx c3,
                                          fn c3' =>
-                                            (TDisjoint (ai, c1', c2', c3'), loc))))
+                                            (CDisjoint (ai, c1', c2', c3'), loc))))
               | TRecord c =>
                 S.map2 (mfc ctx c,
                         fn c' =>
@@ -147,14 +147,6 @@
                          S.map2 (mfc (bind (ctx, Rel (x, k))) c,
                               fn c' =>
                                  (CAbs (x, k', c'), loc)))
-              | CDisjoint (c1, c2, c3) =>
-                S.bind2 (mfc ctx c1,
-                      fn c1' =>
-                         S.bind2 (mfc ctx c2,
-                              fn c2' =>
-                                 S.map2 (mfc ctx c3,
-                                         fn c3' =>
-                                            (CDisjoint (c1', c2', c3'), loc))))
 
               | CName _ => S.return2 cAll
 
diff -r 3c0feecd057d -r b85e6ba56618 src/elaborate.sml
--- a/src/elaborate.sml	Thu Sep 18 15:01:01 2008 -0400
+++ b/src/elaborate.sml	Sat Oct 04 15:50:28 2008 -0400
@@ -225,7 +225,7 @@
             checkKind env t' tk ktype;
             ((L'.TCFun (e', x, k', t'), loc), ktype, gs)
         end
-      | L.TDisjoint (c1, c2, c) =>
+      | L.CDisjoint (c1, c2, c) =>
         let
             val (c1', k1, gs1) = elabCon (env, denv) c1
             val (c2', k2, gs2) = elabCon (env, denv) c2
@@ -239,7 +239,7 @@
             checkKind env c1' k1 (L'.KRecord ku1, loc);
             checkKind env c2' k2 (L'.KRecord ku2, loc);
 
-            ((L'.TDisjoint (L'.Instantiate, c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4)
+            ((L'.CDisjoint (L'.Instantiate, c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4)
         end
       | L.TRecord c =>
         let
@@ -304,23 +304,6 @@
              gs)
         end
 
-      | L.CDisjoint (c1, c2, c) =>
-        let
-            val (c1', k1, gs1) = elabCon (env, denv) c1
-            val (c2', k2, gs2) = elabCon (env, denv) c2
-
-            val ku1 = kunif loc
-            val ku2 = kunif loc
-
-            val (denv', gs3) = D.assert env denv (c1', c2')
-            val (c', k, gs4) = elabCon (env, denv') c
-        in
-            checkKind env c1' k1 (L'.KRecord ku1, loc);
-            checkKind env c2' k2 (L'.KRecord ku2, loc);
-
-            ((L'.CDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4)
-        end
-
       | L.CName s =>
         ((L'.CName s, loc), kname, [])
 
@@ -476,7 +459,6 @@
     case c of
         L'.TFun _ => ktype
       | L'.TCFun _ => ktype
-      | L'.TDisjoint _ => ktype
       | L'.TRecord _ => ktype
 
       | L'.CRel xn => #2 (E.lookupCRel env xn)
@@ -501,7 +483,7 @@
            | (L'.KError, _) => kerror
            | k => raise CUnify' (CKindof (k, c)))
       | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
-      | L'.CDisjoint (_, _, c) => kindof env c
+      | L'.CDisjoint (_, _, _, c) => kindof env c
 
       | L'.CName _ => kname
 
@@ -541,7 +523,7 @@
             L'.CRecord (_, []) => (Nil, gs)
           | L'.CRecord (_, _ :: _) => (Cons, gs)
           | L'.CConcat ((L'.CRecord (_, _ :: _), _), _) => (Cons, gs)
-          | L'.CDisjoint (_, _, c) =>
+          | L'.CDisjoint (_, _, _, c) =>
             let
                 val (s, gs') = summarizeCon (env, denv) c
             in
@@ -824,7 +806,7 @@
 
 and unifyCons' (env, denv) c1 c2 =
     case (#1 c1, #1 c2) of
-        (L'.TDisjoint (_, x1, y1, t1), L'.TDisjoint (_, x2, y2, t2)) =>
+        (L'.CDisjoint (_, x1, y1, t1), L'.CDisjoint (_, x2, y2, t2)) =>
         let
             val gs1 = unifyCons' (env, denv) x1 x2
             val gs2 = unifyCons' (env, denv) y1 y2
@@ -983,7 +965,7 @@
                                     (L'.TCFun (L'.Explicit, "v", dom,
                                                (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc),
                                                           (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc),
-                                                                    (L'.TDisjoint (L'.Instantiate,
+                                                                    (L'.CDisjoint (L'.Instantiate,
                                                                                    (L'.CRecord
                                                                                         ((L'.KUnit, loc),
                                                                                          [((L'.CRel 2, loc),
@@ -1524,7 +1506,7 @@
                 checkKind env c1' k1 (L'.KRecord ku1, loc);
                 checkKind env c2' k2 (L'.KRecord ku2, loc);
 
-                (e', (L'.TDisjoint (L'.LeaveAlone, c1', c2', t), loc), enD gs1 @ enD gs2 @ enD gs3 @ gs4)
+                (e', (L'.CDisjoint (L'.LeaveAlone, c1', c2', t), loc), enD gs1 @ enD gs2 @ enD gs3 @ gs4)
             end
 
           | L.ERecord xes =>
@@ -2572,7 +2554,6 @@
 
               | TFun (c1, c2) => none c1 andalso none c2
               | TCFun (_, _, _, c) => none c
-              | TDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
               | TRecord c => none c
 
               | CVar ([], x) => x <> self
@@ -2600,7 +2581,6 @@
 
               | TFun (c1, c2) => none c1 andalso pos c2
               | TCFun (_, _, _, c) => pos c
-              | TDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
               | TRecord c => pos c
 
               | CVar _ => true
@@ -2721,7 +2701,7 @@
         fun kind k = k
         fun con c =
             case c of
-                L'.TDisjoint (L'.LeaveAlone, c1, c2, c) => L'.TDisjoint (L'.Instantiate, c1, c2, c)
+                L'.CDisjoint (L'.LeaveAlone, c1, c2, c) => L'.CDisjoint (L'.Instantiate, c1, c2, c)
               | _ => c
     in
         U.Con.map {kind = kind, con = con}
diff -r 3c0feecd057d -r b85e6ba56618 src/explify.sml
--- a/src/explify.sml	Thu Sep 18 15:01:01 2008 -0400
+++ b/src/explify.sml	Sat Oct 04 15:50:28 2008 -0400
@@ -49,7 +49,7 @@
     case c of
         L.TFun (t1, t2) => (L'.TFun (explifyCon t1, explifyCon t2), loc)
       | L.TCFun (_, x, k, t) => (L'.TCFun (x, explifyKind k, explifyCon t), loc)
-      | L.TDisjoint (_, _, _, c) => explifyCon c
+      | L.CDisjoint (_, _, _, c) => explifyCon c
       | L.TRecord c => (L'.TRecord (explifyCon c), loc)
 
       | L.CRel n => (L'.CRel n, loc)
@@ -58,7 +58,6 @@
 
       | L.CApp (c1, c2) => (L'.CApp (explifyCon c1, explifyCon c2), loc)
       | L.CAbs (x, k, c) => (L'.CAbs (x, explifyKind k, explifyCon c), loc)
-      | L.CDisjoint (_, _, c) => explifyCon c
 
       | L.CName s => (L'.CName s, loc)
 
diff -r 3c0feecd057d -r b85e6ba56618 src/source.sml
--- a/src/source.sml	Thu Sep 18 15:01:01 2008 -0400
+++ b/src/source.sml	Sat Oct 04 15:50:28 2008 -0400
@@ -49,7 +49,6 @@
 
        | TFun of con * con
        | TCFun of explicitness * string * kind * con
-       | TDisjoint of con * con * con
        | TRecord of con
 
        | CVar of string list * string
diff -r 3c0feecd057d -r b85e6ba56618 src/source_print.sml
--- a/src/source_print.sml	Thu Sep 18 15:01:01 2008 -0400
+++ b/src/source_print.sml	Sat Oct 04 15:50:28 2008 -0400
@@ -81,15 +81,6 @@
                                                 string "->",
                                                 space,
                                                 p_con c])
-      | TDisjoint (c1, c2, c3) => parenIf par (box [p_con c1,
-                                                    space,
-                                                    string "~",
-                                                    space,
-                                                    p_con c2,
-                                                    space,
-                                                    string "->",
-                                                    space,
-                                                    p_con c3])
       | TRecord (CRecord xcs, _) => box [string "{",
                                          p_list (fn (x, c) =>
                                                     box [p_name x,
diff -r 3c0feecd057d -r b85e6ba56618 src/urweb.grm
--- a/src/urweb.grm	Thu Sep 18 15:01:01 2008 -0400
+++ b/src/urweb.grm	Sat Oct 04 15:50:28 2008 -0400
@@ -530,7 +530,6 @@
 
        | FN cargs DARROW cexp           (#1 (cargs (cexp, (KWild, s (FNleft, cexpright)))))
        | cterm TWIDDLE cterm DARROW cexp(CDisjoint (cterm1, cterm2, cexp), s (cterm1left, cexpright))
-       | cterm TWIDDLE cterm ARROW cexp (TDisjoint (cterm1, cterm2, cexp), s (cterm1left, cexpright))
 
        | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright))