src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 60252 2c468c062589
parent 59970 e9f73d87d904
child 60448 78f3c67bc35e
equal deleted inserted replaced
60251:98754695b421 60252:2c468c062589
    52 
    52 
    53 type fact_override =
    53 type fact_override =
    54   {add : (Facts.ref * Token.src list) list,
    54   {add : (Facts.ref * Token.src list) list,
    55    del : (Facts.ref * Token.src list) list,
    55    del : (Facts.ref * Token.src list) list,
    56    only : bool}
    56    only : bool}
       
    57 
       
    58 val local_thisN = Long_Name.localN ^ Long_Name.separator ^ Auto_Bind.thisN
    57 
    59 
    58 (* gracefully handle huge background theories *)
    60 (* gracefully handle huge background theories *)
    59 val max_facts_for_duplicates = 50000
    61 val max_facts_for_duplicates = 50000
    60 val max_facts_for_complex_check = 25000
    62 val max_facts_for_complex_check = 25000
    61 val max_simps_for_clasimpset = 10000
    63 val max_simps_for_clasimpset = 10000
   497                    is_too_complex (Thm.prop_of th)) then
   499                    is_too_complex (Thm.prop_of th)) then
   498                  accum
   500                  accum
   499                else
   501                else
   500                  let
   502                  let
   501                    fun get_name () =
   503                    fun get_name () =
   502                      if name0 = "" then
   504                      if name0 = "" orelse name0 = local_thisN then
   503                        backquote_thm ctxt th
   505                        backquote_thm ctxt th
   504                      else
   506                      else
   505                        let val short_name = Facts.extern ctxt facts name0 in
   507                        let val short_name = Facts.extern ctxt facts name0 in
   506                          if check_thms short_name then
   508                          if check_thms short_name then
   507                            short_name
   509                            short_name