--- 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 =
--- 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