diff --git a/libs/effects/Effect/File.idr b/libs/effects/Effect/File.idr
index f609e5eab..fdc28edc0 100644
--- a/libs/effects/Effect/File.idr
+++ b/libs/effects/Effect/File.idr
@@ -79,14 +79,14 @@ instance Handler FileIO IO where
                                     k True (FH h)
     handle (FH h) Close      k = do closeFile h
                                     k () ()
-    handle (FH h) ReadLine        k = do Right str <- fread h
+    handle (FH h) ReadLine        k = do Right str <- fGetStr h
                                          -- Need proper error handling!
                                              | Left err => k "" (FH h)
                                          k str (FH h)
-    handle (FH h) (WriteString str) k = do Right () <- fwrite h str
+    handle (FH h) (WriteString str) k = do Right () <- fPutStr h str
                                              | Left err => k () (FH h)
                                            k () (FH h)
-    handle (FH h) EOF             k = do e <- feof h
+    handle (FH h) EOF             k = do e <- fEOF h
                                          k e (FH h)
 
 instance Handler FileIO (IOExcept a) where
@@ -95,14 +95,14 @@ instance Handler FileIO (IOExcept a) where
                                     k True (FH h)
     handle (FH h) Close      k = do ioe_lift $ closeFile h
                                     k () ()
-    handle (FH h) ReadLine        k = do Right str <- ioe_lift $ fread h
+    handle (FH h) ReadLine        k = do Right str <- ioe_lift $ fGetStr h
                                          -- Need proper error handling!
                                              | Left err => k "" (FH h)
                                          k str (FH h)
-    handle (FH h) (WriteString str) k = do Right () <- ioe_lift $ fwrite h str
+    handle (FH h) (WriteString str) k = do Right () <- ioe_lift $ fPutStr h str
                                              | Left err => k () (FH h)
                                            k () (FH h)
-    handle (FH h) EOF             k = do e <- ioe_lift $ feof h
+    handle (FH h) EOF             k = do e <- ioe_lift $ fEOF h
                                          k e (FH h)
 
 -- -------------------------------------------------------------- [ The Effect ]
diff --git a/libs/prelude/Decidable/Equality.idr b/libs/prelude/Decidable/Equality.idr
index be2fb09b4..9ab74b596 100644
--- a/libs/prelude/Decidable/Equality.idr
+++ b/libs/prelude/Decidable/Equality.idr
@@ -178,7 +178,7 @@ instance DecEq Char where
 instance DecEq Integer where
     decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
        where primitiveEq : x = y
-             primitiveEq = believe_me (Refl {x})
+             primitiveEq = really_believe_me (Refl {x})
              postulate primitiveNotEq : x = y -> Void
 
 
diff --git a/libs/prelude/Prelude/File.idr b/libs/prelude/Prelude/File.idr
index 7dc135eb4..e61f64b86 100644
--- a/libs/prelude/Prelude/File.idr
+++ b/libs/prelude/Prelude/File.idr
@@ -92,7 +92,7 @@ data Mode = Read | Write | ReadWrite
 
 ||| Open a file
 ||| @ f the filename
-||| @ m the mode
+||| @ m the mode; either Read, Write, or ReadWrite
 openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)
 openFile f m = fopen f (modeStr m) where
   modeStr Read  = "r"
@@ -143,6 +143,13 @@ fread (FHandle h) = do str <- do_fread h
                           then return (Left FileReadError)
                           else return (Right str)
 
+||| Read a line from a file
+||| @h a file handle which must be open for reading
+fGetLine : (h : File) -> IO (Either FileError String)
+fGetLine = fread
+
+%deprecate fread "Use fGetLine instead"
+
 do_fwrite : Ptr -> String -> IO (Either FileError ())
 do_fwrite h s = do res <- prim_fwrite h s
                    if (res /= 0)
@@ -156,14 +163,31 @@ do_fwrite h s = do res <- prim_fwrite h s
 fwrite : File -> String -> IO (Either FileError ())
 fwrite (FHandle h) s = do_fwrite h s
 
+||| Write a line to a file
+||| @h a file handle which must be open for writing
+||| @str the line to write to the file
+fPutStr : (h : File) -> (str : String) -> IO (Either FileError ())
+fPutStr (FHandle h) s = do_fwrite h s
+
+fPutStrLn : File -> String -> IO (Either FileError ())
+fPutStrLn (FHandle h) s = do_fwrite h (s ++ "\n")
+
+%deprecate fwrite "Use fPutStr instead"
+
 do_feof : Ptr -> IO Int
 do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h
 
 ||| Check if a file handle has reached the end
-feof : File -> IO Bool
-feof (FHandle h) = do eof <- do_feof h
+fEOF : File -> IO Bool
+fEOF (FHandle h) = do eof <- do_feof h
                       return (not (eof == 0))
 
+||| Check if a file handle has reached the end
+feof : File -> IO Bool
+feof = fEOF
+
+%deprecate feof "Use fEOF instead"
+
 fpoll : File -> IO Bool
 fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h
                        return (p > 0)
@@ -181,8 +205,8 @@ readFile fn = do Right h <- openFile fn Read
     partial
     readFile' : File -> String -> IO (Either FileError String)
     readFile' h contents =
-       do x <- feof h
-          if not x then do Right l <- fread h
+       do x <- fEOF h
+          if not x then do Right l <- fGetLine h
                                | Left err => return (Left err)
                            readFile' h (contents ++ l)
                    else return (Right contents)
@@ -192,6 +216,6 @@ writeFile : (filepath : String) -> (contents : String) ->
             IO (Either FileError ())
 writeFile fn contents = do
      Right h <- openFile fn Write | Left err => return (Left err)
-     Right () <- fwrite h contents | Left err => return (Left err)
+     Right () <- fPutStr h contents | Left err => return (Left err)
      closeFile h
      return (Right ())
diff --git a/libs/prelude/Prelude/Interactive.idr b/libs/prelude/Prelude/Interactive.idr
index 33da5e6e3..ccbfcfadb 100644
--- a/libs/prelude/Prelude/Interactive.idr
+++ b/libs/prelude/Prelude/Interactive.idr
@@ -121,9 +121,9 @@ processHandle : File ->
                 (onEOF : a -> String) -> 
                 IO ()
 processHandle h acc onRead onEOF 
-   = if !(feof h)
+   = if !(fEOF h)
         then putStr (onEOF acc)
-        else do Right x <- fread h
+        else do Right x <- fGetLine h
                     | Left err => putStr (onEOF acc)
                 let (out, acc') = onRead acc x
                 putStr out
diff --git a/test/dsl002/test014.idr b/test/dsl002/test014.idr
index 0f2743c6e..eeb135afd 100644
--- a/test/dsl002/test014.idr
+++ b/test/dsl002/test014.idr
@@ -23,12 +23,12 @@ close : FILE p -> Updater ()
 close (OpenH h) = iou (closeFile h)
 
 readLine : FILE Reading -> Reader String
-readLine (OpenH h) = ior (do Right str <- fread h
+readLine (OpenH h) = ior (do Right str <- fGetLine h
                                    | return ""
                              return str)
 
 eof : FILE Reading -> Reader Bool
-eof (OpenH h) = ior (feof h)
+eof (OpenH h) = ior (fEOF h)
 
 syntax rclose [h]    = Update close h
 syntax rreadLine [h] = Use readLine h
diff --git a/test/io001/test004.idr b/test/io001/test004.idr
index 883994911..a9ff70415 100644
--- a/test/io001/test004.idr
+++ b/test/io001/test004.idr
@@ -10,15 +10,15 @@ mwhile t b = do v <- t
 dumpFile : String -> IO ()
 dumpFile fn = do { Right h <- openFile fn Read
                    mwhile (do { -- putStrLn "TEST"
-                                x <- feof h
+                                x <- fEOF h
                                 return (not x) })
-                          (do { Right l <- fread h
+                          (do { Right l <- fGetLine h
                                 putStr l })
                    closeFile h }
 
 main : IO ()
 main = do { Right h <- openFile "testfile" Write
-            fwrite h "Hello!\nWorld!\n...\n3\n4\nLast line\n"
+            fPutStr h "Hello!\nWorld!\n...\n3\n4\nLast line\n"
             closeFile h
             putStrLn "Reading testfile"
             Right f <- readFile "testfile"