src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 52031 9a9238342963
parent 51998 f732a674db1b
child 53501 b49bfa77958a
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu May 16 13:19:27 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu May 16 13:34:13 2013 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4    val ignore_no_atp : bool Config.T
     1.5    val instantiate_inducts : bool Config.T
     1.6    val no_fact_override : fact_override
     1.7 -  val fact_from_ref :
     1.8 +  val fact_of_ref :
     1.9      Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
    1.10      -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
    1.11    val backquote_thm : Proof.context -> thm -> string
    1.12 @@ -119,7 +119,7 @@
    1.13  fun stature_of_thm global assms chained css name th =
    1.14    (scope_of_thm global assms chained th, status_of_thm css name th)
    1.15  
    1.16 -fun fact_from_ref ctxt reserved chained css (xthm as (xref, args)) =
    1.17 +fun fact_of_ref ctxt reserved chained css (xthm as (xref, args)) =
    1.18    let
    1.19      val ths = Attrib.eval_thms ctxt [xthm]
    1.20      val bracket =
    1.21 @@ -502,7 +502,7 @@
    1.22      in
    1.23        (if only then
    1.24           maps (map (fn ((name, stature), th) => ((K name, stature), th))
    1.25 -               o fact_from_ref ctxt reserved chained css) add
    1.26 +               o fact_of_ref ctxt reserved chained css) add
    1.27         else
    1.28           let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
    1.29             all_facts ctxt false ho_atp reserved add chained css