eta-expand all search patterns using schematic place holders
authorhaftmann
Thu Dec 04 16:51:54 2014 +0100 (2014-12-04)
changeset 59098b6ba3adb48e3
parent 59097 4b05ce4c84b0
child 59099 62ee9676b7ed
eta-expand all search patterns using schematic place holders
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Thu Dec 04 16:51:54 2014 +0100
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Thu Dec 04 16:51:54 2014 +0100
     1.3 @@ -218,6 +218,13 @@
     1.4  
     1.5  (* filter_pattern *)
     1.6  
     1.7 +fun expand_abs t =
     1.8 +  let
     1.9 +    val m = Term.maxidx_of_term t + 1;
    1.10 +    val vs = strip_abs_vars t;
    1.11 +    val ts = map_index (fn (k, (_, T)) => Var ((Name.aT, m + k), T)) vs;
    1.12 +  in betapplys (t, ts) end;
    1.13 +
    1.14  fun get_names t = Term.add_const_names t (Term.add_free_names t []);
    1.15  
    1.16  (* Does pat match a subterm of obj? *)
    1.17 @@ -240,12 +247,12 @@
    1.18  
    1.19  fun filter_pattern ctxt pat =
    1.20    let
    1.21 -    val pat_consts = get_names pat;
    1.22 -
    1.23 +    val pat' = (expand_abs o Envir.eta_contract) pat;
    1.24 +    val pat_consts = get_names pat';
    1.25      fun check ((x, thm), NONE) = check ((x, thm), SOME (get_names (Thm.full_prop_of thm)))
    1.26        | check ((_, thm), c as SOME thm_consts) =
    1.27           (if subset (op =) (pat_consts, thm_consts) andalso
    1.28 -            matches_subterm (Proof_Context.theory_of ctxt) (pat, Thm.full_prop_of thm)
    1.29 +            matches_subterm (Proof_Context.theory_of ctxt) (pat', Thm.full_prop_of thm)
    1.30            then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, 0) else NONE, c);
    1.31    in check end;
    1.32