src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 60252 2c468c062589
parent 59970 e9f73d87d904
child 60448 78f3c67bc35e
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun May 03 18:14:11 2015 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun May 03 22:15:29 2015 +0200
     1.3 @@ -55,6 +55,8 @@
     1.4     del : (Facts.ref * Token.src list) list,
     1.5     only : bool}
     1.6  
     1.7 +val local_thisN = Long_Name.localN ^ Long_Name.separator ^ Auto_Bind.thisN
     1.8 +
     1.9  (* gracefully handle huge background theories *)
    1.10  val max_facts_for_duplicates = 50000
    1.11  val max_facts_for_complex_check = 25000
    1.12 @@ -499,7 +501,7 @@
    1.13                 else
    1.14                   let
    1.15                     fun get_name () =
    1.16 -                     if name0 = "" then
    1.17 +                     if name0 = "" orelse name0 = local_thisN then
    1.18                         backquote_thm ctxt th
    1.19                       else
    1.20                         let val short_name = Facts.extern ctxt facts name0 in