--- a/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy	Fri Dec 18 14:23:11 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy	Sat Dec 19 11:05:04 2015 +0100
@@ -89,7 +89,7 @@
  WHILE b DO lift F c (sub\<^sub>1 ` M)
  {F (post ` M)}"
 
-permanent_interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter"
+global_interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter"
 proof
   case goal1
   have "a:A \<Longrightarrow> lift Inter (strip a) A \<le> a"