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
```