# 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