# HG changeset patch
# User blanchet
# Date 1292508737 -3600
# Node ID bd57cf5944cb492669daf2f9161d8a4ccaad5da2
# Parent  1393514094d78b3707597ac20432f0670c4a0d79
get rid of experimental feature of term patterns in relevance filter -- doesn't work well unless we take into consideration the equality theory entailed by the relevant facts

diff -r 1393514094d7 -r bd57cf5944cb src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Dec 16 15:12:17 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Dec 16 15:12:17 2010 +0100
@@ -53,8 +53,7 @@
 val trace = Unsynchronized.ref false
 fun trace_msg msg = if !trace then tracing (msg ()) else ()
 
-(* experimental features *)
-val term_patterns = false
+(* experimental feature *)
 val respect_no_atp = true
 
 datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
@@ -241,21 +240,13 @@
   | pattern_for_type (TFree (s, _)) = PApp (s, [])
   | pattern_for_type (TVar _) = PVar
 
-fun pterm thy t =
-  case strip_comb t of
-    (Const x, ts) => PApp (pconst thy true x ts)
-  | (Free x, ts) => PApp (pconst thy false x ts)
-  | (Var _, []) => PVar
-  | _ => PApp ("?", [])  (* equivalence class of higher-order constructs *)
 (* Pairs a constant with the list of its type instantiations. *)
-and ptype thy const x ts =
+fun ptype thy const x =
   (if const then map pattern_for_type (these (try (Sign.const_typargs thy) x))
-   else []) @
-  (if term_patterns then map (pterm thy) ts else [])
-and pconst thy const (s, T) ts = (s, ptype thy const (s, T) ts)
-and rich_ptype thy const (s, T) ts =
-  PType (order_of_type T, ptype thy const (s, T) ts)
-and rich_pconst thy const (s, T) ts = (s, rich_ptype thy const (s, T) ts)
+   else [])
+fun rich_ptype thy const (s, T) =
+  PType (order_of_type T, ptype thy const (s, T))
+fun rich_pconst thy const (s, T) = (s, rich_ptype thy const (s, T))
 
 fun string_for_hyper_pconst (s, ps) =
   s ^ "{" ^ commas (map string_for_ptype ps) ^ "}"
@@ -283,7 +274,7 @@
        introduce a fresh constant to simulate the effect of Skolemization. *)
     fun do_const const x ts =
       (not (is_built_in_const x ts)
-       ? add_pconst_to_table also_skolems (rich_pconst thy const x ts))
+       ? add_pconst_to_table also_skolems (rich_pconst thy const x))
       #> fold do_term ts
     and do_term t =
       case strip_comb t of
@@ -376,7 +367,7 @@
   let
     fun do_const const (s, T) ts =
       (* Two-dimensional table update. Constant maps to types maps to count. *)
-      PType_Tab.map_default (rich_ptype thy const (s, T) ts, 0) (Integer.add 1)
+      PType_Tab.map_default (rich_ptype thy const (s, T), 0) (Integer.add 1)
       |> Symtab.map_default (s, PType_Tab.empty)
       #> fold do_term ts
     and do_term t =