# HG changeset patch
# User wenzelm
# Date 1436189685 -7200
# Node ID 263a8f15faf3844f79b6b5fb31b3b3eaeafa5325
# Parent  143ac4d9504af0dd348751127387f2b32da9f61b
proper outer syntax category, e.g. relevant for PIDE markup;

diff -r 143ac4d9504a -r 263a8f15faf3 src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Mon Jul 06 14:27:03 2015 +0200
+++ b/src/Pure/Tools/find_consts.ML	Mon Jul 06 15:34:45 2015 +0200
@@ -134,9 +134,9 @@
 local
 
 val criterion =
-  Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Strict ||
   Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
-  Parse.xname >> Loose;
+  Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.typ) >> Strict ||
+  Parse.typ >> Loose;
 
 val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);