update for Isabelle2020

4 files changed, 6 insertions, 5 deletions

diff --git a/README.md b/README.md
index 879b5d3..a5b7ef5 100644
--- a/README.md
+++ b/README.md
@@ -4,11 +4,11 @@ An experimental implementation of [homotopy type theory](https://en.wikipedia.or
 
 ### Usage
 
-Isabelle/HoTT is compatible with Isabelle2019.
-To use, add the Isabelle/HoTT folder path to `.isabelle/Isabelle2019/ROOTS` (on Mac/Linux/cygwin installations):
+Isabelle/HoTT is compatible with Isabelle2020.
+To use, add the Isabelle/HoTT folder path to `.isabelle/Isabelle2020/ROOTS` (on Mac/Linux/cygwin installations):
 
 ```
-echo <path/to/Isabelle/HoTT> >> ~/.isabelle/Isabelle2019/ROOTS
+echo <path/to/Isabelle/HoTT> >> ~/.isabelle/Isabelle2020/ROOTS
 ```
 
 ### What (and why) is this?
diff --git a/ROOT b/ROOT
index 218dc9c..09e3042 100644
--- a/ROOT
+++ b/ROOT
@@ -22,3 +22,4 @@ session HoTT in hott = Spartan +
   theories
     Base
     Nat
+
diff --git a/spartan/lib/equality.ML b/spartan/lib/equality.ML
index 79b4086..023147b 100644
--- a/spartan/lib/equality.ML
+++ b/spartan/lib/equality.ML
@@ -84,7 +84,7 @@ fun equality_context_tac fact ctxt =
         THEN ALLGOALS (side_conds_tac ctxt)
       )
   in
-    fn (ctxt, st) => Method.CONTEXT (record_inserts ctxt) (tac st)
+    fn (ctxt, st) => Context_Tactic.TACTIC_CONTEXT (record_inserts ctxt) (tac st)
   end
 
 end
diff --git a/spartan/lib/goals.ML b/spartan/lib/goals.ML
index ce23751..9f394f0 100644
--- a/spartan/lib/goals.ML
+++ b/spartan/lib/goals.ML
@@ -31,7 +31,7 @@ fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt =
   let
     val (stmt, elems_ctxt) = prep_stmt raw_elems raw_stmt ctxt
     val prems = Assumption.local_prems_of elems_ctxt ctxt
-    val stmt_ctxt = fold (fold (Variable.auto_fixes o fst) o snd)
+    val stmt_ctxt = fold (fold (Proof_Context.augment o fst) o snd)
       stmt elems_ctxt
   in
     case raw_stmt of