diff --git a/crucible-mir/CHANGELOG.md b/crucible-mir/CHANGELOG.md
index 45d832b11..9ce7236a6 100644
--- a/crucible-mir/CHANGELOG.md
+++ b/crucible-mir/CHANGELOG.md
@@ -1,3 +1,13 @@
+# next -- TBA
+
+* The calling sequence of ```translateMIR``` has changed: the first argument,
+  which should always have been passed as ```mempty```, has been removed.
+  This will require adjustments in any downstream callers.
+* The corresponding implicit argument in the ```Pass``` type has been removed.
+* The Semigroup and Monoid instances for Collection, CollectionState, and
+  RustModule have been removed. It is not expected that there are any
+  downstream users.
+
 # 0.3 -- 2024-08-30
 
 * Implement byte-to-char casts.
diff --git a/crucible-mir/src/Mir/Generator.hs b/crucible-mir/src/Mir/Generator.hs
index a4640cb7c..08b6f8ac6 100644
--- a/crucible-mir/src/Mir/Generator.hs
+++ b/crucible-mir/src/Mir/Generator.hs
@@ -395,19 +395,6 @@ $(return [])
 
 -- ** Operations and instances
 
-instance Semigroup RustModule where
-  (RustModule cs1 cm1 ex1) <> (RustModule cs2 cm2 ex2) =
-    RustModule (cs1 <> cs2) (cm1 <> cm2) (ex1 <> ex2)
-instance Monoid RustModule where
-  mempty  = RustModule mempty mempty mempty
-
-instance Semigroup CollectionState  where
-  (CollectionState hm1 vm1 sm1 dm1 chm1 col1) <> (CollectionState hm2 vm2 sm2 dm2 chm2 col2) =
-      (CollectionState (hm1 <> hm2) (vm1 <> vm2) (sm1 <> sm2) (dm1 <> dm2) (Map.unionWith (<>) chm1 chm2) (col1 <> col2))
-instance Monoid CollectionState where
-  mempty  = CollectionState mempty mempty mempty mempty mempty mempty
-
-
 instance Show (MirExp s) where
     show (MirExp tr e) = (show e) ++ ": " ++ (show tr)
 
diff --git a/crucible-mir/src/Mir/Mir.hs b/crucible-mir/src/Mir/Mir.hs
index 27b9a953e..8f1dada0f 100644
--- a/crucible-mir/src/Mir/Mir.hs
+++ b/crucible-mir/src/Mir/Mir.hs
@@ -585,18 +585,6 @@ makeLenses ''Instance
 makeLenses ''NamedTy
 makeWrapped ''Substs
 
---------------------------------------------------------------------------------------
--- Other instances for ADT types
---------------------------------------------------------------------------------------
-
-instance Semigroup Collection where
-  (Collection f1 a1 a1' t1 s1 v1 n1 tys1 r1) <> (Collection f2 a2 a2' t2 s2 v2 n2 tys2 r2) =
-    Collection (f1 <> f2) (a1 <> a2) (a1' <> a2') (t1 <> t2) (s1 <> s2) (v1 <> v2) (n1 <> n2) (tys1 <> tys2) (r1 <> r2)
-instance Monoid Collection where
-  mempty  = Collection mempty mempty mempty mempty mempty mempty mempty mempty mempty
-
-
-
 --------------------------------------------------------------------------------------
 --- aux functions ---
 --------------------------------------------------------------------------------------
diff --git a/crucible-mir/src/Mir/ParseTranslate.hs b/crucible-mir/src/Mir/ParseTranslate.hs
index fd1b5d75a..ca48514ce 100644
--- a/crucible-mir/src/Mir/ParseTranslate.hs
+++ b/crucible-mir/src/Mir/ParseTranslate.hs
@@ -69,8 +69,8 @@ uninternMir col = uninternTys unintern (col { _namedTys = mempty })
 
 -- | Translate a MIR collection to Crucible
 translateMIR :: (HasCallStack, ?debug::Int, ?assertFalseOnError::Bool, ?printCrucible::Bool)
-   => CollectionState -> Collection -> C.HandleAllocator -> IO RustModule
-translateMIR lib col halloc =
+   => Collection -> C.HandleAllocator -> IO RustModule
+translateMIR col halloc =
   let ?customOps = Mir.customOps in
-  let col0 = let ?mirLib  = lib^.collection in rewriteCollection col
-  in let ?libCS = lib in transCollection col0 halloc
+  let col0 = rewriteCollection col
+  in transCollection col0 halloc
diff --git a/crucible-mir/src/Mir/Pass.hs b/crucible-mir/src/Mir/Pass.hs
index 02b6496c2..3c12bab09 100644
--- a/crucible-mir/src/Mir/Pass.hs
+++ b/crucible-mir/src/Mir/Pass.hs
@@ -23,7 +23,7 @@ import Mir.Pass.AllocateEnum ( passAllocateEnum )
 
 import Debug.Trace
 
-type Pass = (?debug::Int, ?mirLib::Collection, HasCallStack) => Collection -> Collection
+type Pass = (?debug::Int, HasCallStack) => Collection -> Collection
 
 --------------------------------------------------------------------------------------
 infixl 0 |>
diff --git a/crucible-mir/src/Mir/Pass/AllocateEnum.hs b/crucible-mir/src/Mir/Pass/AllocateEnum.hs
index 240c347c9..34c6d55d2 100644
--- a/crucible-mir/src/Mir/Pass/AllocateEnum.hs
+++ b/crucible-mir/src/Mir/Pass/AllocateEnum.hs
@@ -41,9 +41,9 @@ and replace them with a single aggregate assignment
 
 
 
-passAllocateEnum :: (HasCallStack, ?debug::Int, ?mirLib::Collection) => Collection -> Collection
+passAllocateEnum :: (HasCallStack, ?debug::Int) => Collection -> Collection
 passAllocateEnum col =
-  let ?col = ?mirLib <> col in
+  let ?col = col in
   col & functions %~ fmap (& fbody %~ mblocks %~ map pcr)
 
 
diff --git a/crucible-mir/src/Mir/Trans.hs b/crucible-mir/src/Mir/Trans.hs
index deb29494d..cb6b0fb03 100644
--- a/crucible-mir/src/Mir/Trans.hs
+++ b/crucible-mir/src/Mir/Trans.hs
@@ -2249,7 +2249,7 @@ mkCrateHashesMap
 -- | transCollection: translate a MIR collection
 transCollection ::
     (HasCallStack, ?debug::Int, ?assertFalseOnError::Bool,
-     ?libCS::CollectionState, ?customOps::CustomOpMap,
+     ?customOps::CustomOpMap,
      ?printCrucible::Bool)
     => M.Collection
     -> FH.HandleAllocator
@@ -2286,14 +2286,14 @@ transCollection col halloc = do
         colState = CollectionState hmap vm sm dm chm col
 
     -- translate all of the functions
-    fnInfo <- mapM (stToIO . transDefine (?libCS <> colState)) (Map.elems (col^.M.functions))
+    fnInfo <- mapM (stToIO . transDefine colState) (Map.elems (col^.M.functions))
     let pairs1 = [(name, cfg) | (name, cfg, _) <- fnInfo]
     let transInfo = Map.fromList [(name, fti) | (name, _, fti) <- fnInfo]
-    pairs2 <- mapM (stToIO . transVtable (?libCS <> colState)) (Map.elems (col^.M.vtables))
+    pairs2 <- mapM (stToIO . transVtable colState) (Map.elems (col^.M.vtables))
 
     pairs3 <- Maybe.catMaybes <$> mapM (\intr -> case intr^.M.intrInst of
         Instance (IkVirtual dynTraitName methodIndex) methodId _substs ->
-            stToIO $ Just <$> transVirtCall (?libCS <> colState)
+            stToIO $ Just <$> transVirtCall colState
                 (intr^.M.intrName) methodId dynTraitName methodIndex
         _ -> return Nothing) (Map.elems (col ^. M.intrinsics))
 
diff --git a/crux-mir/src/Mir/Language.hs b/crux-mir/src/Mir/Language.hs
index 1b0eeb45f..2190917af 100644
--- a/crux-mir/src/Mir/Language.hs
+++ b/crux-mir/src/Mir/Language.hs
@@ -253,7 +253,7 @@ runTestsWithExtraOverrides bindExtra (cruxOpts, mirOpts) = do
 
     -- Translate to crucible
     halloc  <- C.newHandleAllocator
-    mir     <- translateMIR mempty col halloc
+    mir     <- translateMIR col halloc
 
     C.AnyCFG staticInitCfg <- transStatics (mir^.rmCS) halloc
     let hi = C.cfgHandle staticInitCfg