16 files changed, 10 insertions, 12 deletions
diff --git a/spartan/core/Spartan.thy b/mltt/core/MLTT.thy
index 5046b6a..18bd2b7 100644
--- a/spartan/core/Spartan.thy
+++ b/mltt/core/MLTT.thy
@@ -1,6 +1,4 @@
-text \<open>Spartan type theory\<close>
-
-theory Spartan
+theory MLTT
 imports
   Pure
   "HOL-Eisbach.Eisbach"
@@ -511,14 +509,14 @@ Lemma snd_comp [comp]:
 subsection \<open>Notation\<close>
 
 definition fst_i ("fst")
-  where [implicit]: "fst \<equiv> Spartan.fst {} {}"
+  where [implicit]: "fst \<equiv> MLTT.fst {} {}"
 
 definition snd_i ("snd")
-  where [implicit]: "snd \<equiv> Spartan.snd {} {}"
+  where [implicit]: "snd \<equiv> MLTT.snd {} {}"
 
 translations
-  "fst" \<leftharpoondown> "CONST Spartan.fst A B"
-  "snd" \<leftharpoondown> "CONST Spartan.snd A B"
+  "fst" \<leftharpoondown> "CONST MLTT.fst A B"
+  "snd" \<leftharpoondown> "CONST MLTT.snd A B"
 
 subsection \<open>Projections\<close>
 
@@ -541,10 +539,10 @@ method snd for p::o = rule snd[where ?p=p]
 
 text \<open>Double projections:\<close>
 
-definition [implicit]: "p\<^sub>1\<^sub>1 p \<equiv> Spartan.fst {} {} (Spartan.fst {} {} p)"
-definition [implicit]: "p\<^sub>1\<^sub>2 p \<equiv> Spartan.snd {} {} (Spartan.fst {} {} p)"
-definition [implicit]: "p\<^sub>2\<^sub>1 p \<equiv> Spartan.fst {} {} (Spartan.snd {} {} p)"
-definition [implicit]: "p\<^sub>2\<^sub>2 p \<equiv> Spartan.snd {} {} (Spartan.snd {} {} p)"
+definition [implicit]: "p\<^sub>1\<^sub>1 p \<equiv> MLTT.fst {} {} (MLTT.fst {} {} p)"
+definition [implicit]: "p\<^sub>1\<^sub>2 p \<equiv> MLTT.snd {} {} (MLTT.fst {} {} p)"
+definition [implicit]: "p\<^sub>2\<^sub>1 p \<equiv> MLTT.fst {} {} (MLTT.snd {} {} p)"
+definition [implicit]: "p\<^sub>2\<^sub>2 p \<equiv> MLTT.snd {} {} (MLTT.snd {} {} p)"
 
 translations
   "CONST p\<^sub>1\<^sub>1 p" \<leftharpoondown> "fst (fst p)"
diff --git a/spartan/core/calc.ML b/mltt/core/calc.ML
index 67dc7fc..67dc7fc 100644
--- a/spartan/core/calc.ML
+++ b/mltt/core/calc.ML
diff --git a/spartan/core/cases.ML b/mltt/core/cases.ML
index 560a9f1..560a9f1 100644
--- a/spartan/core/cases.ML
+++ b/mltt/core/cases.ML
diff --git a/spartan/core/comp.ML b/mltt/core/comp.ML
index 2e50753..2e50753 100644
--- a/spartan/core/comp.ML
+++ b/mltt/core/comp.ML
diff --git a/spartan/core/context_facts.ML b/mltt/core/context_facts.ML
index 5aa7c70..5aa7c70 100644
--- a/spartan/core/context_facts.ML
+++ b/mltt/core/context_facts.ML
diff --git a/spartan/core/context_tactical.ML b/mltt/core/context_tactical.ML
index d0fed61..d0fed61 100644
--- a/spartan/core/context_tactical.ML
+++ b/mltt/core/context_tactical.ML
diff --git a/spartan/core/elaborated_statement.ML b/mltt/core/elaborated_statement.ML
index 33f88cf..33f88cf 100644
--- a/spartan/core/elaborated_statement.ML
+++ b/mltt/core/elaborated_statement.ML
diff --git a/spartan/core/elaboration.ML b/mltt/core/elaboration.ML
index 9e5e0bd..9e5e0bd 100644
--- a/spartan/core/elaboration.ML
+++ b/mltt/core/elaboration.ML
diff --git a/spartan/core/elimination.ML b/mltt/core/elimination.ML
index cf9d21e..cf9d21e 100644
--- a/spartan/core/elimination.ML
+++ b/mltt/core/elimination.ML
diff --git a/spartan/core/eqsubst.ML b/mltt/core/eqsubst.ML
index 5ae8c73..5ae8c73 100644
--- a/spartan/core/eqsubst.ML
+++ b/mltt/core/eqsubst.ML
diff --git a/spartan/core/focus.ML b/mltt/core/focus.ML
index b963cfe..b963cfe 100644
--- a/spartan/core/focus.ML
+++ b/mltt/core/focus.ML
diff --git a/spartan/core/goals.ML b/mltt/core/goals.ML
index 7d52495..7d52495 100644
--- a/spartan/core/goals.ML
+++ b/mltt/core/goals.ML
diff --git a/spartan/core/implicits.ML b/mltt/core/implicits.ML
index 2b63f49..2b63f49 100644
--- a/spartan/core/implicits.ML
+++ b/mltt/core/implicits.ML
diff --git a/spartan/core/lib.ML b/mltt/core/lib.ML
index e43ad98..e43ad98 100644
--- a/spartan/core/lib.ML
+++ b/mltt/core/lib.ML
diff --git a/spartan/core/tactics.ML b/mltt/core/tactics.ML
index 923a3a7..6876d5c 100644
--- a/spartan/core/tactics.ML
+++ b/mltt/core/tactics.ML
@@ -129,7 +129,7 @@ fun elim_ctac tms =
                 |> filter (fn (_, i) => i > 0)
                 (*`t1: T1` comes before `t2: T2` if T1 contains t2 as subterm.
                   If they are incomparable, then order by decreasing
-                  `subterm_count [p, x, y] T`*)
+                  `subterm_count_distinct tms T`*)
                 |> sort (fn (((t1, _), i), ((_, T2), j)) =>
                     Lib.cond_order (Lib.subterm_order T2 t1) (int_ord (j, i)))
                 |> map (#1 o #1)
diff --git a/spartan/core/types.ML b/mltt/core/types.ML
index 5e0d484..5e0d484 100644
--- a/spartan/core/types.ML
+++ b/mltt/core/types.ML