# HG changeset patch
# User blanchet
# Date 1277471283 -7200
# Node ID 02e4ccd512b647eba331543a36397a674b453330
# Parent  9ca40dff25bd6102d13b298e9c4609f5f7415809
further reduce dependencies on "sledgehammer_fact_filter.ML"

diff -r 9ca40dff25bd -r 02e4ccd512b6 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 15:01:35 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 15:08:03 2010 +0200
@@ -16,8 +16,6 @@
      only: bool}
 
   val use_natural_form : bool Unsynchronized.ref
-  val name_thms_pair_from_ref :
-    Proof.context -> thm list -> Facts.ref -> string * thm list
   val relevant_facts :
     bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override
     -> Proof.context * (thm list * 'a) -> thm list -> cnf_thm list
@@ -459,15 +457,6 @@
                                    " theorems")))
   #> filter is_named
 
-fun name_thms_pair_from_ref ctxt chained_ths xref =
-  let
-    val ths = ProofContext.get_fact ctxt xref
-    val name = Facts.string_of_ref xref
-               |> forall (member Thm.eq_thm chained_ths) ths
-                  ? prefix chained_prefix
-  in (name, ths) end
-
-
 (***************************************************************)
 (* ATP invocation methods setup                                *)
 (***************************************************************)
diff -r 9ca40dff25bd -r 02e4ccd512b6 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Fri Jun 25 15:01:35 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Fri Jun 25 15:08:03 2010 +0200
@@ -13,6 +13,8 @@
   val chained_prefix: string
   val trace: bool Unsynchronized.ref
   val trace_msg: (unit -> string) -> unit
+  val name_thms_pair_from_ref :
+    Proof.context -> thm list -> Facts.ref -> string * thm list
   val skolem_theory_name: string
   val skolem_prefix: string
   val skolem_infix: string
@@ -45,12 +47,18 @@
 val trace = Unsynchronized.ref false;
 fun trace_msg msg = if !trace then tracing (msg ()) else ();
 
+fun name_thms_pair_from_ref ctxt chained_ths xref =
+  let
+    val ths = ProofContext.get_fact ctxt xref
+    val name = Facts.string_of_ref xref
+               |> forall (member Thm.eq_thm chained_ths) ths
+                  ? prefix chained_prefix
+  in (name, ths) end
+
 val skolem_theory_name = sledgehammer_prefix ^ "Sko"
 val skolem_prefix = "sko_"
 val skolem_infix = "$"
 
-fun freeze_thm th = #1 (Drule.legacy_freeze_thaw th);
-
 val type_has_topsort = Term.exists_subtype
   (fn TFree (_, []) => true
     | TVar (_, []) => true
@@ -301,7 +309,8 @@
    Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
 fun skolem_theorem_of_def inline def =
   let
-      val (c, rhs) = Thm.dest_equals (cprop_of (freeze_thm def))
+      val (c, rhs) = def |> Drule.legacy_freeze_thaw |> #1 |> cprop_of
+                         |> Thm.dest_equals
       val rhs' = rhs |> inline ? (snd o Thm.dest_comb)
       val (ch, frees) = c_variant_abs_multi (rhs', [])
       val (chilbert, cabs) = ch |> Thm.dest_comb
diff -r 9ca40dff25bd -r 02e4ccd512b6 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 25 15:01:35 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 25 15:08:03 2010 +0200
@@ -18,7 +18,6 @@
 struct
 
 open Sledgehammer_Util
-open Sledgehammer_Fact_Filter
 open Sledgehammer_Fact_Preprocessor
 open ATP_Manager
 open ATP_Systems