--- a/src/HOL/Import/HOL_Light/Compatibility.thy Sat Mar 03 22:37:41 2012 +0100 +++ b/src/HOL/Import/HOL_Light/Compatibility.thy Sat Mar 03 22:37:56 2012 +0100 @@ -347,3 +347,4 @@ by (simp add: INFINITE_def_raw) end +