Implement Makarius's suggestion for improved type pattern parsing.
authorTimothy Bourke
Tue Mar 03 12:14:52 2009 +1100 (2009-03-03)
changeset 30207c56d27155041
parent 30206 48507466d9d2
child 30212 4b35b0f85b42
child 30224 79136ce06bdb
Implement Makarius's suggestion for improved type pattern parsing.
src/Pure/Tools/find_consts.ML
     1.1 --- a/src/Pure/Tools/find_consts.ML	Mon Mar 02 18:11:39 2009 +1100
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Tue Mar 03 12:14:52 2009 +1100
     1.3 @@ -89,7 +89,13 @@
     1.4        if member (op =) (Consts.the_tags consts nm) Markup.property_internal
     1.5        then NONE else SOME low_ranking;
     1.6  
     1.7 -    fun make_pattern crit = ProofContext.read_term_pattern ctxt ("_::" ^ crit) |> type_of;
     1.8 +    fun make_pattern crit =
     1.9 +      let
    1.10 +        val raw_T = Syntax.parse_typ ctxt crit;
    1.11 +        val t = Syntax.check_term
    1.12 +                  (ProofContext.set_mode ProofContext.mode_pattern ctxt)
    1.13 +                  (Term.dummy_pattern raw_T);
    1.14 +      in Term.type_of t end;
    1.15  
    1.16      fun make_match (Strict arg) =
    1.17            let val qty = make_pattern arg; in