diff --git a/README.bin b/README.bin
index 533abae..64b712a 100644
--- a/README.bin
+++ b/README.bin
@@ -1,15 +1,15 @@
 
-You should be able to run HCPL from the unpacked directory with: `./hcpl
-file.hcpl'.  Type `./hcpl --help' for a list of options. It is important
-that you always run ipl from its directory, otherwise it won't start
-because it won't find the standard library in `lib/'. To test whether
-ipl works on your system you may run `scripts/run-tests.sh'. To edit
-*.hcpl files, it is recommended to use the Kate text editor. Syntax
-highlighting files for Kate may be installed with:
-`scripts/install-kate-files.sh'.
+You should be able to run HCPL from the unpacked directory with:
+`./hcpl file.hcpl'.  Type `./hcpl --help' for a list of options. It is
+important that you always run hcpl from its directory, otherwise it
+won't start because it won't find the standard library in `lib/'. To
+test whether hcpl works on your system you may run
+`scripts/run-tests.sh'. To edit *.hcpl files, it is recommended to use
+the Kate text editor. Syntax highlighting files for Kate may be
+installed with: `scripts/install-kate-files.sh'.
 
 The `examples/' subdirectory contains commented examples which form a
-tutorial introduction to IPL. Some knowledge of logic and functional
+tutorial introduction to HCPL. Some knowledge of logic and functional
 programming is necessary to understand them. You should read the
 examples in their numerical order. In case the highlighting does not
 work, there are also html versions of the examples.
diff --git a/lib/logic.hcpl b/lib/logic.hcpl
index 5c950cf..d99d0d3 100644
--- a/lib/logic.hcpl
+++ b/lib/logic.hcpl
@@ -1,4 +1,4 @@
-/* logic.ipl: Illative logic implementation.
+/* logic.hcpl: Illative logic implementation.
  *
  * Copyright (C) 2013 by Lukasz Czajka
  */
diff --git a/lib/logic/core-logic.hcpl b/lib/logic/core-logic.hcpl
index 419ff6a..11d1631 100644
--- a/lib/logic/core-logic.hcpl
+++ b/lib/logic/core-logic.hcpl
@@ -1,4 +1,4 @@
-/* core-logic.ipl: Illative logic rules. This is the 'kernel' of the logic
+/* core-logic.hcpl: Illative logic rules. This is the 'kernel' of the logic
  * implementation. This file implements all basic reasoning rules. All other
  * rules and tactics are supposed to use rules from this file and NOT use
  * 'proof-of', and NOT use definitions from this file which are not a part
diff --git a/lib/logic/derived.hcpl b/lib/logic/derived.hcpl
index 7c25ad5..74122d2 100644
--- a/lib/logic/derived.hcpl
+++ b/lib/logic/derived.hcpl
@@ -1,4 +1,4 @@
-/* derived.ipl: Derived rules and lemmas which don't require standard proof
+/* derived.hcpl: Derived rules and lemmas which don't require standard proof
  * tactics.
  *
  * Copyright (C) 2013 by Lukasz Czajka
diff --git a/lib/logic/derived2.hcpl b/lib/logic/derived2.hcpl
index d49ced2..bbba2a7 100644
--- a/lib/logic/derived2.hcpl
+++ b/lib/logic/derived2.hcpl
@@ -1,4 +1,4 @@
-/* derived2.ipl: Derived rules and lemmas which require standard proof tactics.
+/* derived2.hcpl: Derived rules and lemmas which require standard proof tactics.
  *
  * Copyright (C) 2013 by Lukasz Czajka
  */
diff --git a/lib/logic/macros.hcpl b/lib/logic/macros.hcpl
index de6b399..7002fb5 100644
--- a/lib/logic/macros.hcpl
+++ b/lib/logic/macros.hcpl
@@ -1,4 +1,4 @@
-/* macros.ipl: Convenience logic macros.
+/* macros.hcpl: Convenience logic macros.
  *
  * Copyright (C) 2013 by Lukasz Czajka
  */
@@ -30,7 +30,7 @@ macro axiom = \args {
    | %_ -> error "axiom: wrong arguments"
 }
 
-let __ipl_ex_all_aux = \args \quant \msg {
+let __hcpl_ex_all_aux = \args \quant \msg {
    match List.split-once (== #< : >#) args with
    | [%lst1, %lst2] ->
       begin
@@ -62,8 +62,8 @@ let __ipl_ex_all_aux = \args \quant \msg {
    | %_ -> error msg
 }
 
-macro ex = \args { __ipl_ex_all_aux args #< EX ># "ex: wrong arguments" }
-macro all = \args { __ipl_ex_all_aux args #< ALL ># "all: wrong arguments" }
+macro ex = \args { __hcpl_ex_all_aux args #< EX ># "ex: wrong arguments" }
+macro all = \args { __hcpl_ex_all_aux args #< ALL ># "all: wrong arguments" }
 
 
 macro(0) last = \_ #< (hd facts) >#
diff --git a/lib/tactics/auto-type.hcpl b/lib/tactics/auto-type.hcpl
index 51e3b98..1b3c784 100644
--- a/lib/tactics/auto-type.hcpl
+++ b/lib/tactics/auto-type.hcpl
@@ -1,4 +1,4 @@
-/* auto-type.ipl: Automatic typing proof tactic.
+/* auto-type.hcpl: Automatic typing proof tactic.
  *
  * Copyright (C) 2013 by Lukasz Czajka
  */
diff --git a/lib/tactics/auto.hcpl b/lib/tactics/auto.hcpl
index 0053c4f..b6763e3 100644
--- a/lib/tactics/auto.hcpl
+++ b/lib/tactics/auto.hcpl
@@ -1,4 +1,4 @@
-/* auto.ipl: Automatic proof tactic.
+/* auto.hcpl: Automatic proof tactic.
  *
  * Copyright (C) 2013 by Lukasz Czajka
  */
diff --git a/lib/tactics/fact.hcpl b/lib/tactics/fact.hcpl
index 633a147..28ac42b 100644
--- a/lib/tactics/fact.hcpl
+++ b/lib/tactics/fact.hcpl
@@ -1,4 +1,4 @@
-/* fact.ipl: 'fact' proof tactic.
+/* fact.hcpl: 'fact' proof tactic.
  *
  * Copyright (C) 2013 by Lukasz Czajka
  */
diff --git a/src/builtins/core_builtins.ml b/src/builtins/core_builtins.ml
index 346f4fc..d8e86d6 100644
--- a/src/builtins/core_builtins.ml
+++ b/src/builtins/core_builtins.ml
@@ -88,16 +88,6 @@ let xmatch lst =
 
 (* quoting etc *)
 
-let ipl_quote lst =
-  match lst with
-  | [Closure(x, env, _)] ->
-      Quote.quote x env
-  | [LambdaClosure(body, env, env_len, call_type, times_entered, attrs)] ->
-      Quote.quote (Lambda(body, env_len, call_type, times_entered, attrs)) env
-  | [x] ->
-      Quote.quote x Env.empty
-  | _ -> assert false
-
 let mark lst =
   match lst with
   | y :: Quoted(x) :: _ ->