diff --git a/src/SI/SI_Accepted.thy b/src/SI/SI_Accepted.thy
index bb91b64..ab8c9b3 100644
--- a/src/SI/SI_Accepted.thy
+++ b/src/SI/SI_Accepted.thy
@@ -23,6 +23,7 @@ abbreviation "tonne \<equiv> 10^3 \<odot> kilogram"
 
 subsection \<open> Examples \<close>
 
+declare[[show_types]]
 lemma "watt \<^bold>\<cdot> hour \<cong>\<^sub>Q 3600 \<odot> joule"
   by (si_calc)
 
diff --git a/src/SI/SI_Derived.thy b/src/SI/SI_Derived.thy
index 5640f75..a45183e 100644
--- a/src/SI/SI_Derived.thy
+++ b/src/SI/SI_Derived.thy
@@ -31,7 +31,7 @@ definition [si_eq]: "gram = milli \<odot> kilogram"
 
 text\<open>The full beauty of the approach is perhaps revealed here, with the 
      type of a classical three-dimensional gravitation field:\<close>
-type_synonym gravitation_field = "(real\<^sup>3 \<Rightarrow> real\<^sup>3)[L \<cdot> T\<^sup>-\<^sup>2]"
+type_synonym gravitation_field = "real\<^sup>3[L] \<Rightarrow> (real\<^sup>3[L \<cdot> T\<^sup>-\<^sup>2])"
 
 subsection \<open> Properties \<close>
 
diff --git a/src/SI/SI_Quantities.thy b/src/SI/SI_Quantities.thy
index 3b7a250..8e57cc3 100644
--- a/src/SI/SI_Quantities.thy
+++ b/src/SI/SI_Quantities.thy
@@ -1,7 +1,7 @@
 section \<open> SI Quantities \<close>
 
 theory SI_Quantities
-  imports SI_Units Optics.Lenses
+  imports SI_Units (* Optics.Lenses *)
 begin
 
 
diff --git a/src/SI/SI_Units.thy b/src/SI/SI_Units.thy
index 8b4c998..47c5880 100644
--- a/src/SI/SI_Units.thy
+++ b/src/SI/SI_Units.thy
@@ -217,11 +217,13 @@ subsubsection \<open> SI base type constructors \<close>
 
 text\<open>We embed the basic SI types into the SI type expressions: \<close>
 
+
 instantiation Length :: si_baseunit
 begin
 definition si_sem_Length :: "Length itself \<Rightarrow> Unit" 
   where [si_def]: "si_sem_Length x = 1\<lparr>Meters := 1\<rparr>"
-instance by (intro_classes, auto simp add: si_sem_Length_def is_BaseUnit_def, (transfer, simp)+)
+instance
+  by (intro_classes, auto simp add: si_sem_Length_def is_BaseUnit_def, (transfer, simp)+)
 end
 
 instantiation Mass :: si_baseunit