src/Pure/Syntax/syntax.ML

   datatype 'a trrule =
     ParseRule of 'a * 'a |
     PrintRule of 'a * 'a |
     ParsePrintRule of 'a * 'a
   val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
+  val is_const: syntax -> string -> bool
   val standard_unparse_term: (string -> xstring) ->
     Proof.context -> syntax -> bool -> term -> Pretty.T
   val standard_unparse_typ: Proof.context -> syntax -> typ -> Pretty.T
   val standard_unparse_sort: Proof.context -> syntax -> sort -> Pretty.T
   val update_type_gram: (string * int * mixfix) list -> syntax -> syntax

 fun print_rule (ParseRule _) = NONE
   | print_rule (PrintRule pats) = SOME (swap pats)
   | print_rule (ParsePrintRule pats) = SOME (swap pats);
 
 
+fun is_const (Syntax ({consts, ...}, _)) c = member (op =) consts c;
+
 local
 
 fun check_rule (rule as (lhs, rhs)) =
   (case Ast.rule_error rule of
     SOME msg =>

         Ast.str_of_ast lhs ^ "  ->  " ^ Ast.str_of_ast rhs)
   | NONE => rule);
 
 fun read_pattern ctxt is_logtype syn (root, str) =
   let
-    val Syntax ({consts, ...}, _) = syn;
-
     fun constify (ast as Ast.Constant _) = ast
       | constify (ast as Ast.Variable x) =
-          if member (op =) consts x orelse Long_Name.is_qualified x then Ast.Constant x
+          if is_const syn x orelse Long_Name.is_qualified x then Ast.Constant x
           else ast
       | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
 
     val (syms, pos) = read_token str;
   in