src/Pure/drule.ML
changeset 42471 593289343c7d
parent 40722 441260986b63
child 43324 2b47822868e4
--- 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 =