src/Pure/Tools/find_theorems.ML
changeset 33301 1fe9fc908ec3
parent 33290 6dcb0a970783
child 33381 81269c72321a
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Thu Oct 29 11:26:47 2009 +0100
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Thu Oct 29 11:56:02 2009 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4      (bool * string criterion) list -> unit
     1.5  end;
     1.6  
     1.7 -structure FindTheorems: FIND_THEOREMS =
     1.8 +structure Find_Theorems: FIND_THEOREMS =
     1.9  struct
    1.10  
    1.11  (** search criteria **)
    1.12 @@ -28,24 +28,22 @@
    1.13    Pattern of 'term;
    1.14  
    1.15  fun apply_dummies tm =
    1.16 -  strip_abs tm
    1.17 -  |> fst
    1.18 -  |> map (Term.dummy_pattern o snd)
    1.19 -  |> betapplys o pair tm
    1.20 -  |> (fn x => Term.replace_dummy_patterns x 1)
    1.21 -  |> fst;
    1.22 +  let
    1.23 +    val (xs, _) = Term.strip_abs tm;
    1.24 +    val tm' = Term.betapplys (tm, map (Term.dummy_pattern o #2) xs);
    1.25 +  in #1 (Term.replace_dummy_patterns tm' 1) end;
    1.26  
    1.27  fun parse_pattern ctxt nm =
    1.28    let
    1.29 -    val nm' = case Syntax.parse_term ctxt nm of Const (n, _) => n | _ => nm;
    1.30      val consts = ProofContext.consts_of ctxt;
    1.31 +    val nm' =
    1.32 +      (case Syntax.parse_term ctxt nm of
    1.33 +        Const (c, _) => c
    1.34 +      | _ => Consts.intern consts nm);
    1.35    in
    1.36 -    nm'
    1.37 -    |> Consts.intern consts
    1.38 -    |> Consts.the_abbreviation consts
    1.39 -    |> snd
    1.40 -    |> apply_dummies
    1.41 -    handle TYPE _ => ProofContext.read_term_pattern ctxt nm
    1.42 +    (case try (Consts.the_abbreviation consts) nm' of
    1.43 +      SOME (_, rhs) => apply_dummies rhs
    1.44 +    | NONE => ProofContext.read_term_pattern ctxt nm)
    1.45    end;
    1.46  
    1.47  fun read_criterion _ (Name name) = Name name