# 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