unused untyped exprs
[darcs-mirror-polyfix.git] / SimpleFT.hs
index 5a3d81e..15324e1 100644 (file)
@@ -30,8 +30,6 @@ freeTheorem' e1 e2 (Arrow t1 t2) | isTuple t1 = do
        -- the inner variables names
        fillTuplevars False t1 $ \tve1 -> 
                fillTuplevars True t1 $ \tve2 ->  do
-                       let ve1 = unTypeExpr tve1
-                            ve2 = unTypeExpr tve2
                        cond  <- freeTheorem' (tve1) (tve2) t1
                        concl <- freeTheorem' (app e1 tve1) (app e2 tve2) t2
                        return $ Condition [tve1, tve2] cond concl
@@ -77,7 +75,7 @@ freeTheorem' e1 e2 t@(TPair t1 t2)
                        (TypedExpr x2 tx2)
                        (TypedExpr y2 ty2)
                        t2
-               return $ And concl1 concl2
+               return $ aand concl1 concl2
        | otherwise
           = getVars 4 $ \[x1',x2',y1',y2'] -> do
                let x1 = TypedExpr (Var x1') tx1
@@ -88,7 +86,7 @@ freeTheorem' e1 e2 t@(TPair t1 t2)
                concl2 <- freeTheorem' x2 y2 t2
                return $ unpackPair x1 x2 e1 $
                                unpackPair y1 y2 e2  $
-                                       And concl1 concl2
+                                       aand concl1 concl2
  where (TPair tx1 tx2) = typeOf e1
        (TPair ty1 ty2) = typeOf e2