# 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;