--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Mon Jan 11 21:21:02 2016 +0100
@@ -1273,10 +1273,20 @@
consts inverse :: "'a \<Rightarrow> 'a"
-defs (overloaded)
-inverse_bool: "inverse (b::bool) \<equiv> \<not> b"
-inverse_set: "inverse (S::'a set) \<equiv> -S"
-inverse_pair: "inverse p \<equiv> (inverse (fst p), inverse (snd p))"
+overloading inverse_bool \<equiv> "inverse :: bool \<Rightarrow> bool"
+begin
+ definition "inverse (b::bool) \<equiv> \<not> b"
+end
+
+overloading inverse_set \<equiv> "inverse :: 'a set \<Rightarrow> 'a set"
+begin
+ definition "inverse (S::'a set) \<equiv> -S"
+end
+
+overloading inverse_pair \<equiv> "inverse :: 'a \<times> 'b \<Rightarrow> 'a \<times> 'b"
+begin
+ definition "inverse_pair p \<equiv> (inverse (fst p), inverse (snd p))"
+end
lemma "inverse b"
nitpick [expect = genuine]