diff --git a/group_theory/basic.hlean b/group_theory/basic.hlean
index 9da1d98..34ed39d 100644
--- a/group_theory/basic.hlean
+++ b/group_theory/basic.hlean
@@ -10,12 +10,13 @@ Basic group theory
 /-
   Groups are defined in the HoTT library in algebra/group, as part of the algebraic hierarchy.
   However, there is currently no group theory.
+  The only relevant defintions are the trivial group (in types/unit) and some files in algebra/
 -/
 
-import types.pointed types.pi algebra.bundled
+import algebra.group types.pointed types.pi
 
 open eq algebra pointed function is_trunc pi
-set_option class.force_new true
+
 namespace group
 
   definition pointed_Group [instance] (G : Group) : pointed G := pointed.mk one
diff --git a/group_theory/constructions.hlean b/group_theory/constructions.hlean
index 39dd861..6f6b558 100644
--- a/group_theory/constructions.hlean
+++ b/group_theory/constructions.hlean
@@ -10,7 +10,6 @@ import .basic hit.set_quotient types.sigma types.list types.sum
 
 open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function
      equiv
-set_option class.force_new true
 namespace group
 
   /- Subgroups -/