diff --git a/src/ecSection.ml b/src/ecSection.ml
index bf98fdd8c..ca838b20b 100644
--- a/src/ecSection.ml
+++ b/src/ecSection.ml
@@ -1478,12 +1478,12 @@ and generalize_ctheory
 
     match compiled with
     | None ->
-      genenv
+      { genenv_tmp with tg_env = genenv.tg_env }
     | Some compiled when List.is_empty compiled.ctheory.cth_items ->
-      genenv
+      { genenv_tmp with tg_env = genenv.tg_env }
     | Some compiled ->
       let scenv = add_th ~import:true compiled genenv.tg_env in
-      { genenv with tg_env = scenv; }
+      { genenv_tmp with tg_env = scenv; }
 
 and generalize_lc_item (genenv : to_gen) (prefix : path) (item : sc_item) =
   match item with
diff --git a/tests/theory-in-section-w-declare-type.ec b/tests/theory-in-section-w-declare-type.ec
new file mode 100644
index 000000000..c814936ba
--- /dev/null
+++ b/tests/theory-in-section-w-declare-type.ec
@@ -0,0 +1,12 @@
+section.
+declare type t.
+theory T.
+op foo : t.
+end T.
+op bar : t = T.foo.
+end section.
+
+lemma L (y x : unit): (idfun bar = y) =>
+idfun T.foo = x /\ idfun bar = y.
+move => yP.
+rewrite yP.