insist in explicit overloading;

--- a/src/HOL/TLA/Init.thy	Fri Jul 04 17:19:03 2014 +0200
+++ b/src/HOL/TLA/Init.thy	Fri Jul 04 17:41:35 2014 +0200
@@ -34,6 +34,8 @@
 
 defs
   Init_def:    "sigma |= Init F  ==  (first_world sigma) |= F"
+
+defs (overloaded)
   fw_temp_def: "first_world == %sigma. sigma"
   fw_stp_def:  "first_world == st1"
   fw_act_def:  "first_world == %sigma. (st1 sigma, st2 sigma)"

--- a/src/Pure/theory.ML	Fri Jul 04 17:19:03 2014 +0200
+++ b/src/Pure/theory.ML	Fri Jul 04 17:41:35 2014 +0200
@@ -262,7 +262,8 @@
     else if Type.raw_instance (declT, T') then
       error (message true "imposes additional sort constraints on the constant declaration")
     else if overloaded then ()
-    else warning (message false "is strictly less general than the declared type")
+    else
+      error (message false "is strictly less general than the declared type (overloading required)")
   end;