# HG changeset patch
# User haftmann
# Date 1417708314 -3600
# Node ID 3100a7b1c092993c41ef89fd5422e525c471c08b
# Parent  9ced35b4a2a961dfb3c507274e349c246d04fbe8
turn application-specific Pattern.matches_subterm into an application-private function

diff -r 9ced35b4a2a9 -r 3100a7b1c092 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Thu Dec 04 16:51:54 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Thu Dec 04 16:51:54 2014 +0100
@@ -239,6 +239,16 @@
 
 fun get_names t = Term.add_const_names t (Term.add_free_names t []);
 
+(* Does pat match a subterm of obj? *)
+fun matches_subterm thy (pat, obj) =
+  let
+    fun msub bounds obj = Pattern.matches thy (pat, obj) orelse
+      (case obj of
+        Abs (x, T, t) => msub (bounds + 1) (snd (Term.dest_abs (Name.bound bounds, T, t)))
+      | t $ u => msub bounds t orelse msub bounds u
+      | _ => false)
+  in msub 0 obj end;
+
 (*Including all constants and frees is only sound because matching
   uses higher-order patterns. If full matching were used, then
   constants that may be subject to beta-reduction after substitution
@@ -254,7 +264,7 @@
     fun check ((x, thm), NONE) = check ((x, thm), SOME (get_names (Thm.full_prop_of thm)))
       | check ((_, thm), c as SOME thm_consts) =
          (if subset (op =) (pat_consts, thm_consts) andalso
-            Pattern.matches_subterm (Proof_Context.theory_of ctxt) (pat, Thm.full_prop_of thm)
+            matches_subterm (Proof_Context.theory_of ctxt) (pat, Thm.full_prop_of thm)
           then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, 0) else NONE, c);
   in check end;
 
diff -r 9ced35b4a2a9 -r 3100a7b1c092 src/Pure/more_pattern.ML
--- a/src/Pure/more_pattern.ML	Thu Dec 04 16:51:54 2014 +0100
+++ b/src/Pure/more_pattern.ML	Thu Dec 04 16:51:54 2014 +0100
@@ -11,7 +11,6 @@
   val matches: theory -> term * term -> bool
   val matchess: theory -> term list * term list -> bool
   val equiv: theory -> term * term -> bool
-  val matches_subterm: theory -> term * term -> bool
   val first_order: term -> bool
   val pattern: term -> bool
   val match_rew: theory -> term -> term * term -> (term * term) option
@@ -32,17 +31,6 @@
 
 fun equiv thy (t, u) = matches thy (t, u) andalso matches thy (u, t);
 
-
-(* Does pat match a subterm of obj? *)
-fun matches_subterm thy (pat, obj) =
-  let
-    fun msub bounds obj = matches thy (pat, obj) orelse
-      (case obj of
-        Abs (x, T, t) => msub (bounds + 1) (snd (Term.dest_abs (Name.bound bounds, T, t)))
-      | t $ u => msub bounds t orelse msub bounds u
-      | _ => false)
-  in msub 0 obj end;
-
 fun first_order (Abs (_, _, t)) = first_order t
   | first_order (Var _ $ _) = false
   | first_order (t $ u) = first_order t andalso first_order u