# HG changeset patch
# User wenzelm
# Date 1404488495 -7200
# Node ID 8f1dc3b2daa5efbe22c586477831144086d2cda8
# Parent  cca0db87b653c8a125449976d214ec294a82700d
insist in explicit overloading;

diff -r cca0db87b653 -r 8f1dc3b2daa5 src/HOL/TLA/Init.thy
--- 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)"
diff -r cca0db87b653 -r 8f1dc3b2daa5 src/Pure/theory.ML
--- 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;