diff --git a/Automated_Stateful_Protocol_Verification/Stateful_Protocol_Model.thy b/Automated_Stateful_Protocol_Verification/Stateful_Protocol_Model.thy
index 7810497..da7dd5a 100644
--- a/Automated_Stateful_Protocol_Verification/Stateful_Protocol_Model.thy
+++ b/Automated_Stateful_Protocol_Verification/Stateful_Protocol_Model.thy
@@ -1765,7 +1765,7 @@ proof -
       "prefix (B@[\<langle>\<theta> x != \<theta> y\<rangle>]) (unlabel (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<theta>))) \<or>
        prefix (B@[\<langle>\<theta> y != \<theta> x\<rangle>]) (unlabel (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<theta>)))"
     unfolding prefix_def
-    by (metis (no_types, hide_lams) append.assoc append_Cons append_Nil split_list)
+    by (metis (no_types, opaque_lifting) append.assoc append_Cons append_Nil split_list)
   thus ?thesis
     using \<I> strand_sem_append_stateful[of IK DB _ _ \<I>]
           stateful_strand_sem_NegChecks_no_bvars(2)
@@ -2550,7 +2550,7 @@ proof -
     hence "\<exists>a. \<Gamma> (Var x) = TAtom a"
       by simp
     hence "\<exists>a. \<Gamma> (Fun f T) = TAtom a"
-      by (metis (no_types, hide_lams) \<I>' welltyped_constraint_model_def fT_p wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def)
+      by (metis (no_types, opaque_lifting) \<I>' welltyped_constraint_model_def fT_p wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def)
     ultimately show "(\<exists>f. \<I> x = Fun f []) \<or> (\<exists>y. \<I> x = Var y)"
       using TAtom_term_cases fT_p by metis
   qed
@@ -3762,7 +3762,7 @@ proof (induction \<A> rule: reachable_constraints.induct)
         by (metis IH n(1))
       thus ?thesis
         using n x_nin_\<A> trms\<^sub>s\<^sub>s\<^sub>t_unlabel_prefix_subset(1)[of B]
-        by (metis (no_types, hide_lams) self_append_conv subset_iff subterms\<^sub>s\<^sub>e\<^sub>t_mono prefix_def)
+        by (metis (no_types, opaque_lifting) self_append_conv subset_iff subterms\<^sub>s\<^sub>e\<^sub>t_mono prefix_def)
     qed (use n x_nin_\<A> in fastforce)
   qed
 
diff --git a/Automated_Stateful_Protocol_Verification/Stateful_Protocol_Verification.thy b/Automated_Stateful_Protocol_Verification/Stateful_Protocol_Verification.thy
index 6a9d519..0041078 100644
--- a/Automated_Stateful_Protocol_Verification/Stateful_Protocol_Verification.thy
+++ b/Automated_Stateful_Protocol_Verification/Stateful_Protocol_Verification.thy
@@ -2296,7 +2296,7 @@ proof -
       moreover 
       have "\<alpha> y = Var z"
         using zn
-        by (metis (no_types, hide_lams) \<sigma> subst_compose_def subst_imgI subst_to_var_is_var
+        by (metis (no_types, opaque_lifting) \<sigma> subst_compose_def subst_imgI subst_to_var_is_var
                   term.distinct(1) transaction_fresh_subst_def var_comp(2)) 
       then have "\<alpha> y \<cdot> \<I> = \<I> z"
         by auto
diff --git a/Automated_Stateful_Protocol_Verification/Term_Implication.thy b/Automated_Stateful_Protocol_Verification/Term_Implication.thy
index b0c75d0..e6bbda0 100644
--- a/Automated_Stateful_Protocol_Verification/Term_Implication.thy
+++ b/Automated_Stateful_Protocol_Verification/Term_Implication.thy
@@ -620,7 +620,7 @@ proof -
 
     have "take n S@drop n T = S1@T ! n#T2" "take (Suc n) S@drop (Suc n) T = S1@S ! n#T2"
       using n T S append_eq_conv_conj
-      by (metis, metis (no_types, hide_lams) Cons_nth_drop_Suc append.assoc append_Cons
+      by (metis, metis (no_types, opaque_lifting) Cons_nth_drop_Suc append.assoc append_Cons
                                              append_Nil take_Suc_conv_app_nth) 
     moreover have "(T ! n, S ! n) \<in> timpl_closure' c" using IH Suc.prems by simp
     ultimately show ?case
diff --git a/Automated_Stateful_Protocol_Verification/document/root.tex b/Automated_Stateful_Protocol_Verification/document/root.tex
index b1834c4..cfd4f6a 100644
--- a/Automated_Stateful_Protocol_Verification/document/root.tex
+++ b/Automated_Stateful_Protocol_Verification/document/root.tex
@@ -1,5 +1,6 @@
 \documentclass[10pt,DIV16,a4paper,abstract=true,twoside=semi,openright]
 {scrreprt}
+\usepackage[T1]{fontenc}
 \usepackage[english]{babel}
 \usepackage[numbers, sort&compress]{natbib}
 \usepackage{isabelle,isabellesym}
diff --git a/Automated_Stateful_Protocol_Verification/trac/trac.thy b/Automated_Stateful_Protocol_Verification/trac/trac.thy
index 191c613..5c1ae6a 100644
--- a/Automated_Stateful_Protocol_Verification/trac/trac.thy
+++ b/Automated_Stateful_Protocol_Verification/trac/trac.thy
@@ -279,7 +279,7 @@ structure ml_isar_wrapper = struct
 
    fun prove_simple name stmt tactic lthy = 
      let
-       val thm = Goal.prove lthy [] [] stmt (fn {context, ...} => tactic context) 
+       val thm = Goal.prove lthy [] [] stmt (tactic o #context)
                  |> Goal.norm_result lthy
                  |> Goal.check_finished lthy
      in 
@@ -1646,7 +1646,6 @@ structure trac = struct
   (
     type T = hide_tvar_tab
     val empty  = Symtab.empty:hide_tvar_tab
-    val extend = I
     fun merge(t1,t2)  = merge_trac_tab (t1, t2)
   );