this removes the ugly hack of creating an ad-hoc type alias symbol
for substitutions like "clone T with type t 'a = list (int, 'a)".

If a type symbol "t1 'a 'b 'c" is instantiated into a type of the
form "t2 'a 'b 'c", then the metas that mention the type symbol "t1"
are preserved, and "t1" is replaced with "t2". Otherwise, all such
metas disappear in the cloned theory.