# HG changeset patch
# User wenzelm
# Date 1190579014 -7200
# Node ID c62320337a4e6867465081dab20c68216bce27c7
# Parent  29306b20079ba63f93265cd56bfc9a33a7ce42e6
ProofContext.read_term_pattern;

diff -r 29306b20079b -r c62320337a4e src/Pure/Isar/find_theorems.ML
--- a/src/Pure/Isar/find_theorems.ML	Sun Sep 23 22:23:33 2007 +0200
+++ b/src/Pure/Isar/find_theorems.ML	Sun Sep 23 22:23:34 2007 +0200
@@ -27,10 +27,8 @@
   | read_criterion _ Intro = Intro
   | read_criterion _ Elim = Elim
   | read_criterion _ Dest = Dest
-  | read_criterion ctxt (Simp str) =
-      Simp (hd (ProofContext.read_term_pats dummyT ctxt [str]))
-  | read_criterion ctxt (Pattern str) =
-      Pattern (hd (ProofContext.read_term_pats dummyT ctxt [str]));
+  | read_criterion ctxt (Simp str) = Simp (ProofContext.read_term_pattern ctxt str)
+  | read_criterion ctxt (Pattern str) = Pattern (ProofContext.read_term_pattern ctxt str);
 
 fun pretty_criterion ctxt (b, c) =
   let