# HG changeset patch
# User Timothy Bourke
# Date 1236042892 -39600
# Node ID c56d271550419594bec4f4c0f3bf01ecb83a0777
# Parent  48507466d9d278fe6a38d994be84462f30264597
Implement Makarius's suggestion for improved type pattern parsing.

diff -r 48507466d9d2 -r c56d27155041 src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Mon Mar 02 18:11:39 2009 +1100
+++ b/src/Pure/Tools/find_consts.ML	Tue Mar 03 12:14:52 2009 +1100
@@ -89,7 +89,13 @@
       if member (op =) (Consts.the_tags consts nm) Markup.property_internal
       then NONE else SOME low_ranking;
 
-    fun make_pattern crit = ProofContext.read_term_pattern ctxt ("_::" ^ crit) |> type_of;
+    fun make_pattern crit =
+      let
+        val raw_T = Syntax.parse_typ ctxt crit;
+        val t = Syntax.check_term
+                  (ProofContext.set_mode ProofContext.mode_pattern ctxt)
+                  (Term.dummy_pattern raw_T);
+      in Term.type_of t end;
 
     fun make_match (Strict arg) =
           let val qty = make_pattern arg; in