find_theorems: better handling of abbreviations (by Timothy Bourke)
authorkleing
Wed Oct 21 16:41:22 2009 +1100 (2009-10-21)
changeset 33036c61fe520602b
parent 33035 15eab423e573
child 33039 5018f6a76b3f
find_theorems: better handling of abbreviations (by Timothy Bourke)
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Wed Oct 21 00:36:12 2009 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Wed Oct 21 16:41:22 2009 +1100
     1.3 @@ -27,6 +27,27 @@
     1.4    Name of string | Intro | IntroIff | Elim | Dest | Solves | Simp of 'term |
     1.5    Pattern of 'term;
     1.6  
     1.7 +fun apply_dummies tm =
     1.8 +  strip_abs tm
     1.9 +  |> fst
    1.10 +  |> map (Term.dummy_pattern o snd)
    1.11 +  |> betapplys o pair tm
    1.12 +  |> (fn x => Term.replace_dummy_patterns x 1)
    1.13 +  |> fst;
    1.14 +
    1.15 +fun parse_pattern ctxt nm =
    1.16 +  let
    1.17 +    val nm' = case Syntax.parse_term ctxt nm of Const (n, _) => n | _ => nm;
    1.18 +    val consts = ProofContext.consts_of ctxt;
    1.19 +  in
    1.20 +    nm'
    1.21 +    |> Consts.intern consts
    1.22 +    |> Consts.the_abbreviation consts
    1.23 +    |> snd
    1.24 +    |> apply_dummies
    1.25 +    handle TYPE _ => ProofContext.read_term_pattern ctxt nm
    1.26 +  end;
    1.27 +
    1.28  fun read_criterion _ (Name name) = Name name
    1.29    | read_criterion _ Intro = Intro
    1.30    | read_criterion _ IntroIff = IntroIff
    1.31 @@ -34,7 +55,7 @@
    1.32    | read_criterion _ Dest = Dest
    1.33    | read_criterion _ Solves = Solves
    1.34    | read_criterion ctxt (Simp str) = Simp (ProofContext.read_term_pattern ctxt str)
    1.35 -  | read_criterion ctxt (Pattern str) = Pattern (ProofContext.read_term_pattern ctxt str);
    1.36 +  | read_criterion ctxt (Pattern str) = Pattern (parse_pattern ctxt str);
    1.37  
    1.38  fun pretty_criterion ctxt (b, c) =
    1.39    let