--- 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