# HG changeset patch
# User haftmann
# Date 1417708314 -3600
# Node ID 4b05ce4c84b0e5a788801b5ea592c450d5bda65a
# Parent  15f7ebb29d38b7c3f58d58906817e00dce4b8a81
revert "better" handling of abbreviation from c61fe520602b

diff -r 15f7ebb29d38 -r 4b05ce4c84b0 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Thu Dec 04 16:51:54 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Thu Dec 04 16:51:54 2014 +0100
@@ -31,32 +31,13 @@
 datatype 'term criterion =
   Name of string | Intro | Elim | Dest | Solves | Simp of 'term | Pattern of 'term;
 
-fun apply_dummies tm =
-  let
-    val (xs, _) = Term.strip_abs tm;
-    val tm' = Term.betapplys (tm, map (Term.dummy_pattern o #2) xs);
-  in #1 (Term.replace_dummy_patterns tm' 1) end;
-
-fun parse_pattern ctxt nm =
-  let
-    val consts = Proof_Context.consts_of ctxt;
-    val nm' =
-      (case Syntax.parse_term ctxt nm of
-        Const (c, _) => c
-      | _ => Consts.intern consts nm);
-  in
-    (case try (Consts.the_abbreviation consts) nm' of
-      SOME (_, rhs) => apply_dummies (Proof_Context.expand_abbrevs ctxt rhs)
-    | NONE => Proof_Context.read_term_pattern ctxt nm)
-  end;
-
 fun read_criterion _ (Name name) = Name name
   | read_criterion _ Intro = Intro
   | read_criterion _ Elim = Elim
   | read_criterion _ Dest = Dest
   | read_criterion _ Solves = Solves
   | read_criterion ctxt (Simp str) = Simp (Proof_Context.read_term_pattern ctxt str)
-  | read_criterion ctxt (Pattern str) = Pattern (parse_pattern ctxt str);
+  | read_criterion ctxt (Pattern str) = Pattern (Proof_Context.read_term_pattern ctxt str);
 
 fun pretty_criterion ctxt (b, c) =
   let