1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 15:01:35 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 15:08:03 2010 +0200
     1.3 @@ -16,8 +16,6 @@
     1.4       only: bool}
     1.5  
     1.6    val use_natural_form : bool Unsynchronized.ref
     1.7 -  val name_thms_pair_from_ref :
     1.8 -    Proof.context -> thm list -> Facts.ref -> string * thm list
     1.9    val relevant_facts :
    1.10      bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override
    1.11      -> Proof.context * (thm list * 'a) -> thm list -> cnf_thm list
    1.12 @@ -459,15 +457,6 @@
    1.13                                     " theorems")))
    1.14    #> filter is_named
    1.15  
    1.16 -fun name_thms_pair_from_ref ctxt chained_ths xref =
    1.17 -  let
    1.18 -    val ths = ProofContext.get_fact ctxt xref
    1.19 -    val name = Facts.string_of_ref xref
    1.20 -               |> forall (member Thm.eq_thm chained_ths) ths
    1.21 -                  ? prefix chained_prefix
    1.22 -  in (name, ths) end
    1.23 -
    1.24 -
    1.25  (***************************************************************)
    1.26  (* ATP invocation methods setup                                *)
    1.27  (***************************************************************)

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Fri Jun 25 15:01:35 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Fri Jun 25 15:08:03 2010 +0200
     2.3 @@ -13,6 +13,8 @@
     2.4    val chained_prefix: string
     2.5    val trace: bool Unsynchronized.ref
     2.6    val trace_msg: (unit -> string) -> unit
     2.7 +  val name_thms_pair_from_ref :
     2.8 +    Proof.context -> thm list -> Facts.ref -> string * thm list
     2.9    val skolem_theory_name: string
    2.10    val skolem_prefix: string
    2.11    val skolem_infix: string
    2.12 @@ -45,12 +47,18 @@
    2.13  val trace = Unsynchronized.ref false;
    2.14  fun trace_msg msg = if !trace then tracing (msg ()) else ();
    2.15  
    2.16 +fun name_thms_pair_from_ref ctxt chained_ths xref =
    2.17 +  let
    2.18 +    val ths = ProofContext.get_fact ctxt xref
    2.19 +    val name = Facts.string_of_ref xref
    2.20 +               |> forall (member Thm.eq_thm chained_ths) ths
    2.21 +                  ? prefix chained_prefix
    2.22 +  in (name, ths) end
    2.23 +
    2.24  val skolem_theory_name = sledgehammer_prefix ^ "Sko"
    2.25  val skolem_prefix = "sko_"
    2.26  val skolem_infix = "$"
    2.27  
    2.28 -fun freeze_thm th = #1 (Drule.legacy_freeze_thaw th);
    2.29 -
    2.30  val type_has_topsort = Term.exists_subtype
    2.31    (fn TFree (_, []) => true
    2.32      | TVar (_, []) => true
    2.33 @@ -301,7 +309,8 @@
    2.34     Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
    2.35  fun skolem_theorem_of_def inline def =
    2.36    let
    2.37 -      val (c, rhs) = Thm.dest_equals (cprop_of (freeze_thm def))
    2.38 +      val (c, rhs) = def |> Drule.legacy_freeze_thaw |> #1 |> cprop_of
    2.39 +                         |> Thm.dest_equals
    2.40        val rhs' = rhs |> inline ? (snd o Thm.dest_comb)
    2.41        val (ch, frees) = c_variant_abs_multi (rhs', [])
    2.42        val (chilbert, cabs) = ch |> Thm.dest_comb

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 25 15:01:35 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 25 15:08:03 2010 +0200
     3.3 @@ -18,7 +18,6 @@
     3.4  struct
     3.5  
     3.6  open Sledgehammer_Util
     3.7 -open Sledgehammer_Fact_Filter
     3.8  open Sledgehammer_Fact_Preprocessor
     3.9  open ATP_Manager
    3.10  open ATP_Systems