--- a/src/HOL/IMP/Abs_Int3.thy Fri Dec 18 14:23:11 2015 +0100
+++ b/src/HOL/IMP/Abs_Int3.thy Sat Dec 19 11:05:04 2015 +0100
@@ -256,7 +256,7 @@
end
-permanent_interpretation Abs_Int_wn
+global_interpretation Abs_Int_wn
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
@@ -541,7 +541,7 @@
split: prod.splits if_splits extended.split)
-permanent_interpretation Abs_Int_wn_measure
+global_interpretation Abs_Int_wn_measure
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl