diff --git a/Deduce.lark b/Deduce.lark
index a1f382c..43008ec 100644
--- a/Deduce.lark
+++ b/Deduce.lark
@@ -215,7 +215,6 @@ ident: IDENT              -> ident
  | type_hi
 
 ?type_hi: IDENT   -> type_name
- | "int"          -> int_type
  | "bool"         -> bool_type
  | "type"         -> type_type
  | "(" type ")"   -> paren
diff --git a/README.thm b/README.thm
index 07907a8..cd83f21 100644
--- a/README.thm
+++ b/README.thm
@@ -1,6 +1,6 @@
 This file was automatically generated by Deduce.
 This file summarizes the theorems proved in the file:
-	./README.pf
+	README.pf
 
 search_take: (all xs:List<Nat>. (all y:Nat. not (y ∈ set_of(take(search(xs, y), xs)))))
 
diff --git a/index.md b/index.md
index 3928f95..a19439a 100644
--- a/index.md
+++ b/index.md
@@ -189,12 +189,3 @@ you can use instead.
  -->
 <!--  LocalWords:  contra foo sx xy dist mult
  -->
-
-<!--
-``` {.deduce file=README.pf}
-import List
-import Set
-
-<<search_take>>
-```
--->
diff --git a/proof_checker.py b/proof_checker.py
index 262abbf..96371c4 100644
--- a/proof_checker.py
+++ b/proof_checker.py
@@ -18,7 +18,7 @@
 #    and run the print and assert statements.
 
 from abstract_syntax import *
-from error import error, warning, get_verbose, set_verbose
+from error import error, warning, error_header, get_verbose, set_verbose
 
 imported_modules = set()
 checked_modules = set()
@@ -1515,8 +1515,8 @@ def type_check_call_helper(loc, new_rator, args, env, recfun, subterms, ret_ty,
                 + '\n\t'.join([str(ty) for (x,ty) in overloads]))
       elif num_matches > 1:
           error(loc, 'in call to ' + str(new_rator) + '\n'\
-                + 'ambiguous overloads:\n\t' \
-                + '\n\t'.join([str(ty) for (x,ty) in overloads]))
+                + 'ambiguous overloads:\n' \
+                + '\n'.join([error_header(ty.location) + str(ty) for (x,ty) in overloads]))
       else:
           return new_call
     case FunctionType(loc2, typarams, param_types, return_type):