diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 200a2db25..0b872dc71 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -106,9 +106,8 @@ name const * g_tactic_unfold = nullptr;
 name const * g_tactic_whnf = nullptr;
 name const * g_true = nullptr;
 name const * g_true_intro = nullptr;
-name const * g_truncation = nullptr;
-name const * g_truncation_is_trunc = nullptr;
-name const * g_truncation_nat_to_trunc_index = nullptr;
+name const * g_is_trunc = nullptr;
+name const * g_is_trunc_trunc_index_of_nat = nullptr;
 name const * g_unit = nullptr;
 name const * g_unit_star = nullptr;
 name const * g_well_founded = nullptr;
@@ -216,9 +215,8 @@ void initialize_constants() {
     g_tactic_whnf = new name{"tactic", "whnf"};
     g_true = new name{"true"};
     g_true_intro = new name{"true", "intro"};
-    g_truncation = new name{"truncation"};
-    g_truncation_is_trunc = new name{"truncation", "is_trunc"};
-    g_truncation_nat_to_trunc_index = new name{"truncation", "nat_to_trunc_index"};
+    g_is_trunc = new name{"is_trunc"};
+    g_is_trunc_trunc_index_of_nat = new name{"is_trunc", "trunc_index", "of_nat"};
     g_unit = new name{"unit"};
     g_unit_star = new name{"unit", "star"};
     g_well_founded = new name{"well_founded"};
@@ -327,9 +325,8 @@ void finalize_constants() {
     delete g_tactic_whnf;
     delete g_true;
     delete g_true_intro;
-    delete g_truncation;
-    delete g_truncation_is_trunc;
-    delete g_truncation_nat_to_trunc_index;
+    delete g_is_trunc;
+    delete g_is_trunc_trunc_index_of_nat;
     delete g_unit;
     delete g_unit_star;
     delete g_well_founded;
@@ -437,9 +434,8 @@ name const & get_tactic_unfold_name() { return *g_tactic_unfold; }
 name const & get_tactic_whnf_name() { return *g_tactic_whnf; }
 name const & get_true_name() { return *g_true; }
 name const & get_true_intro_name() { return *g_true_intro; }
-name const & get_truncation_name() { return *g_truncation; }
-name const & get_truncation_is_trunc_name() { return *g_truncation_is_trunc; }
-name const & get_truncation_nat_to_trunc_index_name() { return *g_truncation_nat_to_trunc_index; }
+name const & get_is_trunc_name() { return *g_is_trunc; }
+name const & get_is_trunc_trunc_index_of_nat_name() { return *g_is_trunc_trunc_index_of_nat; }
 name const & get_unit_name() { return *g_unit; }
 name const & get_unit_star_name() { return *g_unit_star; }
 name const & get_well_founded_name() { return *g_well_founded; }
diff --git a/src/library/constants.h b/src/library/constants.h
index a57585bab..0c6dcca58 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -108,9 +108,8 @@ name const & get_tactic_unfold_name();
 name const & get_tactic_whnf_name();
 name const & get_true_name();
 name const & get_true_intro_name();
-name const & get_truncation_name();
-name const & get_truncation_is_trunc_name();
-name const & get_truncation_nat_to_trunc_index_name();
+name const & get_is_trunc_name();
+name const & get_is_trunc_trunc_index_of_nat_name();
 name const & get_unit_name();
 name const & get_unit_star_name();
 name const & get_well_founded_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index 2418c0d0a..b1386632a 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -102,7 +102,6 @@ tactic.whnf
 true
 true.intro
 is_trunc
-is_trunc
 is_trunc.trunc_index.of_nat
 unit
 unit.star
diff --git a/src/library/tactic/class_instance_synth.cpp b/src/library/tactic/class_instance_synth.cpp
index 3b2c945a4..b9969c2b7 100644
--- a/src/library/tactic/class_instance_synth.cpp
+++ b/src/library/tactic/class_instance_synth.cpp
@@ -453,9 +453,9 @@ optional<expr> mk_class_instance(environment const & env, io_state const & ios,
 }
 
 optional<expr> mk_hset_instance(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & type) {
-    expr trunc_index = mk_app(mk_constant(get_truncation_nat_to_trunc_index_name()), mk_constant(get_nat_zero_name()));
+    expr trunc_index = mk_app(mk_constant(get_is_trunc_trunc_index_of_nat_name()), mk_constant(get_nat_zero_name()));
     level lvl        = sort_level(tc.ensure_type(type).first);
-    expr is_hset     = mk_app(mk_constant(get_truncation_is_trunc_name(), {lvl}), trunc_index, type);
+    expr is_hset     = mk_app(mk_constant(get_is_trunc_name(), {lvl}), trunc_index, type);
     return mk_class_instance(tc.env(), ios, ctx, tc.mk_fresh_name(), is_hset);
 }
 }