diff -r 542f2c6da692 -r f6ded81f5690 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Dec 18 14:23:11 2015 +0100
+++ b/src/HOL/Finite_Set.thy	Sat Dec 19 11:05:04 2015 +0100
@@ -1209,7 +1209,7 @@
   But now that we have @{const fold} things are easy:
 \<close>
 
-permanent_interpretation card: folding "\<lambda>_. Suc" 0
+global_interpretation card: folding "\<lambda>_. Suc" 0
   defines card = "folding.F (\<lambda>_. Suc) 0"
   by standard rule