diff --git a/UPF_Firewall/FWNormalisation/NormalisationIPPProofs.thy b/UPF_Firewall/FWNormalisation/NormalisationIPPProofs.thy
index 4c86dd1..e77a722 100644
--- a/UPF_Firewall/FWNormalisation/NormalisationIPPProofs.thy
+++ b/UPF_Firewall/FWNormalisation/NormalisationIPPProofs.thy
@@ -1214,7 +1214,7 @@ next
   case (3 v va vb y z) thus ?case
     apply (cases "z = []", simp_all)
      apply (simp add: PLemmas(8) UPFDefs(8) list2FWpolicyconc sepnMT)
-    by (metis (no_types, hide_lams) Conc_not_MT Cdom2  nlpaux domIff l2p_aux sepnMT)
+    by (metis (no_types, opaque_lifting) Conc_not_MT Cdom2  nlpaux domIff l2p_aux sepnMT)
 next
   case (4 v va y z) thus ?case
     apply (cases "z = []", simp_all)
diff --git a/UPF_Firewall/FWNormalisation/NormalisationIntegerPortProof.thy b/UPF_Firewall/FWNormalisation/NormalisationIntegerPortProof.thy
index c06e525..4e100e8 100644
--- a/UPF_Firewall/FWNormalisation/NormalisationIntegerPortProof.thy
+++ b/UPF_Firewall/FWNormalisation/NormalisationIntegerPortProof.thy
@@ -470,7 +470,7 @@ next
       apply (case_tac "xs = []", simp_all)
       unfolding removeShadowRules1_alternative_def
        apply (case_tac x, simp_all)
-      by (metis (no_types, hide_lams) CConcEnd2 CConcStart C_DenyAll RS1n_nMT aux114 
+      by (metis (no_types, opaque_lifting) CConcEnd2 CConcStart C_DenyAll RS1n_nMT aux114 
           domIff removeShadowRules1_alternative_def 
           removeShadowRules1_alternative_rev.simps(2) rev.simps(2))
     done 
diff --git a/UPF_Firewall/document/root.tex b/UPF_Firewall/document/root.tex
index ea3b54e..30ef07d 100644
--- a/UPF_Firewall/document/root.tex
+++ b/UPF_Firewall/document/root.tex
@@ -1,4 +1,5 @@
 \documentclass[11pt,DIV10,a4paper,twoside=semi,openright,titlepage]{scrreprt}
+\usepackage[T1]{fontenc}
 \usepackage{fixltx2e}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%% Overrides the (rightfully issued) warning by Koma Script that \rm