diff --git a/docs/src/concepts/theories.md b/docs/src/concepts/theories.md
index dd941c14..3cb7d887 100644
--- a/docs/src/concepts/theories.md
+++ b/docs/src/concepts/theories.md
@@ -2,33 +2,8 @@
 
 A theory in GATlab consists of two parts.
 
-1. A Julia value of type `Theory` that describes the theory.
+1. A Julia value of type `GAT` that describes the theory.
 2. A module named by the theory with various Julia types that give us handles
 for metaprogramming.
 
-These metaprogramming types include:
 
-- A singleton struct named `Th` and subtyping `AbstractTheory` that has an
-   overload of `gettheory` on it returning the Julia value from 1. This is used
-   to pass around the entire theory at the type level.
-- A singleton struct for each type constructor and term constructor in the
-   theory. These are used in place of `Lvl` in types, so that backtraces are
-   more readable.
-
-Example:
-
-```julia
-module Category
-using GATlab.Theories
-
-struct Th <: AbstractTheory end
-
-Theories.gettheory(::Th) = ...
-
-struct Ob <: TypCon{1} end
-struct Hom <: TypCon{2} end
-
-struct compose <: TrmCon{3} end
-...
-end
-```
diff --git a/docs/src/stdlib.md b/docs/src/stdlib.md
index b4623239..4fd24cd9 100644
--- a/docs/src/stdlib.md
+++ b/docs/src/stdlib.md
@@ -5,7 +5,7 @@
 Our friend `ThCategory` is the main theory in this module.
 
 ```@docs
-GATlab.Stdlib.StdTheories.Categories.ThCategory
+GATlab.Stdlib.StdTheories.ThCategory
 ```
 
 You can specialize a theory by adding more axioms. In this case we can specialize the theory of categories to that of thin category by adding the axiom that two morphisms are equal if they have the same domain and codomain.
@@ -15,33 +15,30 @@ thineq := f == g :: Hom(A,B) ⊣ [A::Ob, B::Ob, f::Hom(A,B), g::Hom(A,B)]
 ```
 
 ```@docs
-GATlab.Stdlib.StdTheories.Categories.ThThinCategory
+GATlab.Stdlib.StdTheories.ThThinCategory
 ```
 ### Category Building Blocks
 The remaining theories in this module are not necessarily useful, but go to show demonstrate the theory hierarchy can be built up in small increments.
 
 ```@docs
-GATlab.Stdlib.StdTheories.Categories.ThClass
+GATlab.Stdlib.StdTheories.ThClass
 ```
 
 ```@docs
-GATlab.Stdlib.StdTheories.Categories.ThLawlessCat
+GATlab.Stdlib.StdTheories.ThLawlessCat
 ```
 
 ```@docs
-GATlab.Stdlib.StdTheories.Categories.ThAscCat
+GATlab.Stdlib.StdTheories.ThAscCat
 ```
 
 ```@docs
-GATlab.Stdlib.StdTheories.Categories.ThIdLawlessCat
+GATlab.Stdlib.StdTheories.ThIdLawlessCat
 ```
 
 ```@autodocs
 Modules = [GATlab.Stdlib,
   GATlab.Stdlib.StdTheories,
-  GATlab.Stdlib.StdTheories.Algebra,
-  GATlab.Stdlib.StdTheories.Monoidal,
-  GATlab.Stdlib.StdTheories.Naturals,
   GATlab.Stdlib.StdModels,
   GATlab.Stdlib.StdModels.FinSets,
   ]
diff --git a/src/models/Presentations.jl b/src/models/Presentations.jl
index 70dda11a..b1e7fb16 100644
--- a/src/models/Presentations.jl
+++ b/src/models/Presentations.jl
@@ -10,7 +10,7 @@ in applications like knowledge representation.
 module Presentations
 export @present, Presentation, generator, generators, generator_index,
   has_generator, equations, add_generator!, add_generators!, add_definition!,
-  add_equation!, add_equations!, change_theory
+  add_equation!, add_equations!
 
 using Base.Meta: ParseError
 using MLStyle: @match
@@ -49,21 +49,7 @@ function Base.:(==)(pres1::Presentation, pres2::Presentation)
   pres1.syntax == pres2.syntax && pres1.generators == pres2.generators &&
     pres1.equations == pres2.equations
 end
-"""
-Move a presentation to a new syntax,
-duplicating all the data on shared names. In particular,
-this is lossless if all the generators of the original
-presentation are at names in the new syntax.
-"""
-function change_theory(syntax::Module,pres::Presentation{S,Name}) where {S,Name}
-  T = syntax.theory()
-  pres_new = Presentation(syntax)
-  types = intersect(keys(pres_new.generators),keys(pres.generators))
-  for t in types map(pres.generators[t]) do x
-    add_generator!(pres_new,generator_switch_syntax(syntax,x)) end end
-  #XX: test on equations
-  pres_new
-end
+
 function Base.copy(pres::Presentation{T,Name}) where {T,Name}
   Presentation{T,Name}(pres.syntax, map(copy, pres.generators),
                        copy(pres.generator_name_index), copy(pres.equations))
diff --git a/src/syntax/Scopes.jl b/src/syntax/Scopes.jl
index ab6725d5..e9cb32f3 100644
--- a/src/syntax/Scopes.jl
+++ b/src/syntax/Scopes.jl
@@ -352,8 +352,6 @@ struct Scope{T} <: HasScope{T}
   end
 end
 
-Scope(s::Scope) = s
-
 Base.:(==)(s1::Scope, s2::Scope) = s1.tag == s2.tag
 
 Base.hash(s::Scope, h::UInt64) = hash(s.tag, h)
@@ -701,24 +699,6 @@ function ScopeList{T}(scopes::Vector{<:HasScope{T}}) where {T}
   c
 end
 
-function Scope(hsl::ScopeList{T}) where T
-  if nscopes(hsl) == 0
-    Scope{T}() 
-  else 
-    res = Scope{T}()
-    newtag = gettag(res)
-    retagdict = Dict{ScopeTag, ScopeTag}()
-    for nextscope in getscope.(hsl.scopes)
-      retagdict[gettag(nextscope)] = newtag
-      nextscope = retag(retagdict, nextscope)
-      for b in getbindings(nextscope)
-        unsafe_pushbinding!(res, b)
-      end
-    end
-    res
-  end
-end
-
 function Base.copy(c::ScopeList{T}) where {T}
   ScopeList{T}(copy(c.scopes), copy(c.taglookup), copy(c.namelookup))
 end
diff --git a/test/syntax/GATs.jl b/test/syntax/GATs.jl
index d0f67360..47e993bb 100644
--- a/test/syntax/GATs.jl
+++ b/test/syntax/GATs.jl
@@ -65,6 +65,9 @@ c = GATContext(thcat, sortscope)
 HomT = fromexpr(c, :(Hom(A, A)), AlgType)
 HomS = AlgSort(HomT)
 
+@test rename(gettag(sortscope), Dict(:A=>:Z), HomT) isa AlgType
+@test retag(Dict(gettag(sortscope)=>newscopetag()), HomT) isa AlgType
+
 @test sortcheck(c, AlgTerm(A)) == ObS
 
 # # Good term and bad term
@@ -98,6 +101,10 @@ TG = ThGraph.Meta.theory
 @test TG ⊆ T
 @test T ⊈ TG
 
+# ToExpr
+#-------
+toexpr.(Ref(T), T.segments)
+
 # InCtx
 #----------
 # tic = fromexpr(T, :(compose(f,compose(id(b),id(b))) ⊣ [a::Ob, b::Ob, f::Hom(a,b)]), TermInCtx);
diff --git a/test/syntax/Scopes.jl b/test/syntax/Scopes.jl
index 64725a4c..bbce2075 100644
--- a/test/syntax/Scopes.jl
+++ b/test/syntax/Scopes.jl
@@ -90,6 +90,9 @@ bind_X, bind_Y = Binding{String}(:X, Alias(x)), Binding{String}(:Y, Alias(y))
 xy_scope = Scope([bind_x, bind_y, bind_X, bind_Y]; tag=tag1)
 xy_scope′ = Scope([bind_x]; tag=tag1)
 
+@test alltags(retag(Dict(tag1=>tag2),xy_scope)) == Set([tag2])
+@test identvalues(xy_scope′) == [x => "ex"]
+
 @test xy_scope == xy_scope′
 @test hash(xy_scope) == hash(xy_scope′)
 @test basicprinted(xy_scope) == "{$(basicprinted(bind_x)), $(basicprinted(bind_y)), X = x, Y = y}"