src/Pure/Thy/thy_parse.ML
changeset 636 31b36d96f7d6
parent 587 3ba470399605
child 656 ec05d2fdfeee
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Wed Oct 12 16:29:10 1994 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Wed Oct 12 16:30:19 1994 +0100
     1.3 @@ -24,6 +24,7 @@
     1.4    val long_ident: token list -> string * token list
     1.5    val long_id: token list -> string * token list
     1.6    val type_var: token list -> string * token list
     1.7 +  val type_args: token list -> string list * token list
     1.8    val nat: token list -> string * token list
     1.9    val string: token list -> string * token list
    1.10    val verbatim: token list -> string * token list
    1.11 @@ -43,6 +44,7 @@
    1.12    val sort: token list -> string * token list
    1.13    val opt_infix: token list -> string * token list
    1.14    val opt_mixfix: token list -> string * token list
    1.15 +  val opt_witness: token list -> string * token list
    1.16    type syntax
    1.17    val make_syntax: string list ->
    1.18      (string * (token list -> (string * string) * token list)) list -> syntax
    1.19 @@ -56,12 +58,12 @@
    1.20    val pure_sections:
    1.21      (string * (token list -> (string * string) * token list)) list
    1.22    (*items for building strings*)
    1.23 -  val parens	: string -> string   
    1.24 -  val brackets	: string -> string   
    1.25 -  val mk_list	: string list -> string   
    1.26 -  val mk_big_list : string list -> string   
    1.27 -  val mk_pair	: string * string -> string   
    1.28 -  val mk_triple	: string * string * string -> string   
    1.29 +  val parens: string -> string   
    1.30 +  val brackets: string -> string   
    1.31 +  val mk_list: string list -> string   
    1.32 +  val mk_big_list: string list -> string   
    1.33 +  val mk_pair: string * string -> string   
    1.34 +  val mk_triple: string * string * string -> string   
    1.35  end;
    1.36  
    1.37  functor ThyParseFun(structure Symtab: SYMTAB and ThyScan: THY_SCAN): THY_PARSE =
    1.38 @@ -329,8 +331,8 @@
    1.39    >> mk_witness;
    1.40  
    1.41  val instance_decl =
    1.42 -  (name --$$ "<" -- name >> (pair "|> add_inst_subclass" o mk_pair) ||
    1.43 -    name --$$ "::" -- arity >> (pair "|> add_inst_arity" o mk_triple2))
    1.44 +  (name --$$ "<" -- name >> (pair "|> AxClass.add_inst_subclass" o mk_pair) ||
    1.45 +    name --$$ "::" -- arity >> (pair "|> AxClass.add_inst_arity" o mk_triple2))
    1.46    -- opt_witness
    1.47    >> (fn ((x, y), z) => (cat_lines [x, y, z], ""));
    1.48  
    1.49 @@ -459,7 +461,7 @@
    1.50    ("MLtext", verbatim >> rpair ""),
    1.51    axm_section "rules" "|> add_axioms" axiom_decls,
    1.52    axm_section "defs" "|> add_defs" axiom_decls,
    1.53 -  axm_section "axclass" "|> add_axclass" axclass_decl,
    1.54 +  axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
    1.55    ("instance", instance_decl)];
    1.56  
    1.57