# HG changeset patch
# User wenzelm
# Date 1470339020 -7200
# Node ID be0a4a0bf7f519fe8841096ddb66e6711c5ae146
# Parent  d83cb0902e4fcc2c934a044d343340eea9572121
prefer hardwired "nothing";

diff -r d83cb0902e4f -r be0a4a0bf7f5 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Aug 04 21:25:16 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Aug 04 21:30:20 2016 +0200
@@ -1013,11 +1013,12 @@
   | retrieve pick context (Facts.Named ((xname, pos), sel)) =
       let
         val thy = Context.theory_of context;
-        fun immediate thm = {name = xname, dynamic = false, thms = [Thm.transfer thy thm]};
+        fun immediate thms = {name = xname, dynamic = false, thms = map (Thm.transfer thy) thms};
         val {name, dynamic, thms} =
           (case xname of
-            "" => immediate Drule.dummy_thm
-          | "_" => immediate Drule.asm_rl
+            "" => immediate [Drule.dummy_thm]
+          | "_" => immediate [Drule.asm_rl]
+          | "nothing" => immediate []
           | _ => retrieve_generic context (xname, pos));
         val thms' =
           if dynamic andalso Config.get_generic context dynamic_facts_dummy
diff -r d83cb0902e4f -r be0a4a0bf7f5 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Thu Aug 04 21:25:16 2016 +0200
+++ b/src/Pure/pure_thy.ML	Thu Aug 04 21:30:20 2016 +0200
@@ -223,7 +223,6 @@
       \ (CONST Pure.term :: 'a itself => prop) (CONST Pure.type :: 'a itself)"),
     (Binding.make ("conjunction_def", @{here}),
       prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
-  #> Global_Theory.add_thmss [((Binding.make ("nothing", @{here}), []), [])] #> snd
   #> fold (fn (a, prop) =>
       snd o Thm.add_axiom_global (Binding.make (a, @{here}), prop)) Proofterm.equality_axms);