revert "better" handling of abbreviation from c61fe520602b
authorhaftmann
Thu Dec 04 16:51:54 2014 +0100 (2014-12-04)
changeset 590974b05ce4c84b0
parent 59096 15f7ebb29d38
child 59098 b6ba3adb48e3
revert "better" handling of abbreviation from c61fe520602b
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 @@ -31,32 +31,13 @@
     1.4  datatype 'term criterion =
     1.5    Name of string | Intro | Elim | Dest | Solves | Simp of 'term | Pattern of 'term;
     1.6  
     1.7 -fun apply_dummies tm =
     1.8 -  let
     1.9 -    val (xs, _) = Term.strip_abs tm;
    1.10 -    val tm' = Term.betapplys (tm, map (Term.dummy_pattern o #2) xs);
    1.11 -  in #1 (Term.replace_dummy_patterns tm' 1) end;
    1.12 -
    1.13 -fun parse_pattern ctxt nm =
    1.14 -  let
    1.15 -    val consts = Proof_Context.consts_of ctxt;
    1.16 -    val nm' =
    1.17 -      (case Syntax.parse_term ctxt nm of
    1.18 -        Const (c, _) => c
    1.19 -      | _ => Consts.intern consts nm);
    1.20 -  in
    1.21 -    (case try (Consts.the_abbreviation consts) nm' of
    1.22 -      SOME (_, rhs) => apply_dummies (Proof_Context.expand_abbrevs ctxt rhs)
    1.23 -    | NONE => Proof_Context.read_term_pattern ctxt nm)
    1.24 -  end;
    1.25 -
    1.26  fun read_criterion _ (Name name) = Name name
    1.27    | read_criterion _ Intro = Intro
    1.28    | read_criterion _ Elim = Elim
    1.29    | read_criterion _ Dest = Dest
    1.30    | read_criterion _ Solves = Solves
    1.31    | read_criterion ctxt (Simp str) = Simp (Proof_Context.read_term_pattern ctxt str)
    1.32 -  | read_criterion ctxt (Pattern str) = Pattern (parse_pattern ctxt str);
    1.33 +  | read_criterion ctxt (Pattern str) = Pattern (Proof_Context.read_term_pattern ctxt str);
    1.34  
    1.35  fun pretty_criterion ctxt (b, c) =
    1.36    let