# 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