# HG changeset patch
# User wenzelm
# Date 1303580513 -7200
# Node ID 593289343c7d6d0e7d1420ba1aa1cf0c0c6123c1
# Parent  cc78b0ed0fadcefa42a184c3706081f83522d8a5
hardwired mapping "_" -> "Pure.asm_rl" avoids legacy binding;

diff -r cc78b0ed0fad -r 593289343c7d src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sat Apr 23 19:22:11 2011 +0200
+++ b/src/Pure/drule.ML	Sat Apr 23 19:41:53 2011 +0200
@@ -565,7 +565,6 @@
 
 (*The rule V/V, obtains assumption solving for eresolve_tac*)
 val asm_rl = store_standard_thm_open (Binding.name "asm_rl") (Thm.trivial (read_prop "?psi"));
-val _ = store_thm_open (Binding.name "_") asm_rl;
 
 (*Meta-level cut rule: [| V==>W; V |] ==> W *)
 val cut_rl =
diff -r cc78b0ed0fad -r 593289343c7d src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Sat Apr 23 19:22:11 2011 +0200
+++ b/src/Pure/global_theory.ML	Sat Apr 23 19:41:53 2011 +0200
@@ -84,7 +84,10 @@
     val xname = Facts.name_of_ref xthmref;
     val pos = Facts.pos_of_ref xthmref;
 
-    val name = intern_fact thy xname;
+    val name =
+      (case intern_fact thy xname of
+        "_" => "Pure.asm_rl"
+      | name => name);
     val res = Facts.lookup context facts name;
     val _ = Theory.check_thy thy;
   in