src/Pure/Syntax/syntax.ML
changeset 35111 18cd034922ba
parent 33957 e9afca2118d4
child 35130 0991c84e8dcf
     1.1 --- a/src/Pure/Syntax/syntax.ML	Thu Feb 11 22:03:15 2010 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Thu Feb 11 22:03:37 2010 +0100
     1.3 @@ -54,6 +54,7 @@
     1.4      PrintRule of 'a * 'a |
     1.5      ParsePrintRule of 'a * 'a
     1.6    val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
     1.7 +  val is_const: syntax -> string -> bool
     1.8    val standard_unparse_term: (string -> xstring) ->
     1.9      Proof.context -> syntax -> bool -> term -> Pretty.T
    1.10    val standard_unparse_typ: Proof.context -> syntax -> typ -> Pretty.T
    1.11 @@ -592,6 +593,8 @@
    1.12    | print_rule (ParsePrintRule pats) = SOME (swap pats);
    1.13  
    1.14  
    1.15 +fun is_const (Syntax ({consts, ...}, _)) c = member (op =) consts c;
    1.16 +
    1.17  local
    1.18  
    1.19  fun check_rule (rule as (lhs, rhs)) =
    1.20 @@ -603,11 +606,9 @@
    1.21  
    1.22  fun read_pattern ctxt is_logtype syn (root, str) =
    1.23    let
    1.24 -    val Syntax ({consts, ...}, _) = syn;
    1.25 -
    1.26      fun constify (ast as Ast.Constant _) = ast
    1.27        | constify (ast as Ast.Variable x) =
    1.28 -          if member (op =) consts x orelse Long_Name.is_qualified x then Ast.Constant x
    1.29 +          if is_const syn x orelse Long_Name.is_qualified x then Ast.Constant x
    1.30            else ast
    1.31        | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
    1.32