thm "_" = asm_rl;

--- a/src/Pure/drule.ML	Fri Aug 27 15:52:32 1999 +0200
+++ b/src/Pure/drule.ML	Fri Aug 27 18:59:27 1999 +0200
@@ -535,8 +535,8 @@
 (*** Some useful meta-theorems ***)
 
 (*The rule V/V, obtains assumption solving for eresolve_tac*)
-val asm_rl =
-  store_thm "asm_rl" (trivial(read_prop "PROP ?psi"));
+val asm_rl = store_thm "asm_rl" (trivial(read_prop "PROP ?psi"));
+val _ = store_thm "_" asm_rl;
 
 (*Meta-level cut rule: [| V==>W; V |] ==> W *)
 val cut_rl =