obsolete type sg is now an alias for Context.theory;
authorwenzelm
Fri Jun 17 18:33:27 2005 +0200 (2005-06-17)
changeset 164421171ecf7fb7e
parent 16441 92a8a25e53c5
child 16443 82a116532e3e
obsolete type sg is now an alias for Context.theory;
code and interfaces related to stamps and data now in context.ML;
actual signature content declared as theory data;
removed type sg_ref (superceded by theory_ref);
signature SIGN_THEORY lists theory operations that are duplicated in Theory;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Fri Jun 17 18:33:26 2005 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri Jun 17 18:33:27 2005 +0200
     1.3 @@ -2,482 +2,256 @@
     1.4      ID:         $Id$
     1.5      Author:     Lawrence C Paulson and Markus Wenzel
     1.6  
     1.7 -The abstract type "sg" of signatures.
     1.8 +Logical signature content: naming conventions, concrete syntax, type
     1.9 +signature, constant declarations.
    1.10  *)
    1.11  
    1.12 -signature SIGN =
    1.13 +signature SIGN_THEORY =
    1.14  sig
    1.15 -  type sg
    1.16 -  type sg_ref
    1.17 -  type data
    1.18 -  val rep_sg: sg ->
    1.19 -   {self: sg_ref,
    1.20 -    tsig: Type.tsig,
    1.21 -    consts: (typ * stamp) NameSpace.table,
    1.22 -    naming: NameSpace.naming,
    1.23 -    data: data}
    1.24 -  val stamp_names_of: sg -> string list
    1.25 -  val exists_stamp: string -> sg -> bool
    1.26 -  val pretty_sg: sg -> Pretty.T
    1.27 -  val pprint_sg: sg -> pprint_args -> unit
    1.28 -  val pretty_abbrev_sg: sg -> Pretty.T
    1.29 -  val str_of_sg: sg -> string
    1.30 -  val is_stale: sg -> bool
    1.31 -  val self_ref: sg -> sg_ref
    1.32 -  val deref: sg_ref -> sg
    1.33 -  val name_of: sg -> string
    1.34 -  val is_draft: sg -> bool
    1.35 -  val eq_sg: sg * sg -> bool
    1.36 -  val subsig: sg * sg -> bool
    1.37 -  val same_sg: sg * sg -> bool
    1.38 -  val joinable: sg * sg -> bool
    1.39 -  val prep_ext: sg -> sg
    1.40 -  val copy: sg -> sg
    1.41 -  val add_name: string -> sg -> sg
    1.42 -  val data_kinds: data -> string list
    1.43 -  val print_all_data: sg -> unit
    1.44 -  val pre_pure: sg
    1.45 -  val PureN: string
    1.46 -  val CPureN: string
    1.47 -  val naming_of: sg -> NameSpace.naming
    1.48 -  val base_name: string -> bstring
    1.49 -  val full_name: sg -> bstring -> string
    1.50 -  val full_name_path: sg -> string -> bstring -> string
    1.51 -  val declare_name: sg -> string -> NameSpace.T -> NameSpace.T
    1.52 -  val syn_of: sg -> Syntax.syntax
    1.53 -  val tsig_of: sg -> Type.tsig
    1.54 -  val classes: sg -> class list
    1.55 -  val defaultS: sg -> sort
    1.56 -  val subsort: sg -> sort * sort -> bool
    1.57 -  val of_sort: sg -> typ * sort -> bool
    1.58 -  val witness_sorts: sg -> sort list -> sort list -> (typ * sort) list
    1.59 -  val universal_witness: sg -> (typ * sort) option
    1.60 -  val typ_instance: sg -> typ * typ -> bool
    1.61 -  val is_logtype: sg -> string -> bool
    1.62 -  val const_type: sg -> string -> typ option
    1.63 -  val the_const_type: sg -> string -> typ
    1.64 -  val declared_tyname: sg -> string -> bool
    1.65 -  val declared_const: sg -> string -> bool
    1.66 -  val class_space: sg -> NameSpace.T
    1.67 -  val type_space: sg -> NameSpace.T
    1.68 -  val const_space: sg -> NameSpace.T
    1.69 -  val intern_class: sg -> xstring -> string
    1.70 -  val extern_class: sg -> string -> xstring
    1.71 -  val intern_type: sg -> xstring -> string
    1.72 -  val extern_type: sg -> string -> xstring
    1.73 -  val intern_const: sg -> xstring -> string
    1.74 -  val extern_const: sg -> string -> xstring
    1.75 -  val intern_sort: sg -> sort -> sort
    1.76 -  val extern_sort: sg -> sort -> sort
    1.77 -  val intern_typ: sg -> typ -> typ
    1.78 -  val extern_typ: sg -> typ -> typ
    1.79 -  val intern_term: sg -> term -> term
    1.80 -  val extern_term: sg -> term -> term
    1.81 -  val intern_tycons: sg -> typ -> typ
    1.82 -  val pretty_term': Syntax.syntax -> sg -> term -> Pretty.T
    1.83 -  val pretty_term: sg -> term -> Pretty.T
    1.84 -  val pretty_typ: sg -> typ -> Pretty.T
    1.85 -  val pretty_sort: sg -> sort -> Pretty.T
    1.86 -  val pretty_classrel: sg -> class list -> Pretty.T
    1.87 -  val pretty_arity: sg -> arity -> Pretty.T
    1.88 -  val string_of_term: sg -> term -> string
    1.89 -  val string_of_typ: sg -> typ -> string
    1.90 -  val string_of_sort: sg -> sort -> string
    1.91 -  val string_of_classrel: sg -> class list -> string
    1.92 -  val string_of_arity: sg -> arity -> string
    1.93 -  val pprint_term: sg -> term -> pprint_args -> unit
    1.94 -  val pprint_typ: sg -> typ -> pprint_args -> unit
    1.95 -  val pp: sg -> Pretty.pp
    1.96 -  val certify_class: sg -> class -> class
    1.97 -  val certify_sort: sg -> sort -> sort
    1.98 -  val certify_typ: sg -> typ -> typ
    1.99 -  val certify_typ_syntax: sg -> typ -> typ
   1.100 -  val certify_typ_abbrev: sg -> typ -> typ
   1.101 -  val certify_term: Pretty.pp -> sg -> term -> term * typ * int
   1.102 -  val read_sort': Syntax.syntax -> sg -> string -> sort
   1.103 -  val read_sort: sg -> string -> sort
   1.104 -  val read_typ': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
   1.105 -  val read_typ_syntax': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
   1.106 -  val read_typ_abbrev': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
   1.107 -  val read_typ: sg * (indexname -> sort option) -> string -> typ
   1.108 -  val read_typ_syntax: sg * (indexname -> sort option) -> string -> typ
   1.109 -  val read_typ_abbrev: sg * (indexname -> sort option) -> string -> typ
   1.110 -  val read_tyname: sg -> string -> typ
   1.111 -  val read_const: sg -> string -> term
   1.112 -  val infer_types_simult: Pretty.pp -> sg -> (indexname -> typ option) ->
   1.113 -    (indexname -> sort option) -> string list -> bool
   1.114 -    -> (term list * typ) list -> term list * (indexname * typ) list
   1.115 -  val infer_types: Pretty.pp -> sg -> (indexname -> typ option) ->
   1.116 -    (indexname -> sort option) -> string list -> bool
   1.117 -    -> term list * typ -> term * (indexname * typ) list
   1.118 -  val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax ->
   1.119 -    sg * (indexname -> typ option) * (indexname -> sort option) ->
   1.120 -    string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
   1.121 -  val read_def_terms:
   1.122 -    sg * (indexname -> typ option) * (indexname -> sort option) ->
   1.123 -    string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
   1.124 -  val simple_read_term: sg -> typ -> string -> term
   1.125 -  val add_defsort: string -> sg -> sg
   1.126 -  val add_defsort_i: sort -> sg -> sg
   1.127 -  val add_types: (bstring * int * mixfix) list -> sg -> sg
   1.128 -  val add_nonterminals: bstring list -> sg -> sg
   1.129 -  val add_tyabbrs: (bstring * string list * string * mixfix) list -> sg -> sg
   1.130 -  val add_tyabbrs_i: (bstring * string list * typ * mixfix) list -> sg -> sg
   1.131 -  val add_arities: (xstring * string list * string) list -> sg -> sg
   1.132 -  val add_arities_i: (string * sort list * sort) list -> sg -> sg
   1.133 -  val add_syntax: (bstring * string * mixfix) list -> sg -> sg
   1.134 -  val add_syntax_i: (bstring * typ * mixfix) list -> sg -> sg
   1.135 -  val add_modesyntax: (string * bool) * (bstring * string * mixfix) list -> sg -> sg
   1.136 -  val add_modesyntax_i: (string * bool) * (bstring * typ * mixfix) list -> sg -> sg
   1.137 -  val del_modesyntax: (string * bool) * (bstring * string * mixfix) list -> sg -> sg
   1.138 -  val del_modesyntax_i: (string * bool) * (bstring * typ * mixfix) list -> sg -> sg
   1.139 -  val add_consts: (bstring * string * mixfix) list -> sg -> sg
   1.140 -  val add_consts_i: (bstring * typ * mixfix) list -> sg -> sg
   1.141 -  val const_of_class: class -> string
   1.142 -  val class_of_const: string -> class
   1.143 -  val add_classes: (bstring * xstring list) list -> sg -> sg
   1.144 -  val add_classes_i: (bstring * class list) list -> sg -> sg
   1.145 -  val add_classrel: (xstring * xstring) list -> sg -> sg
   1.146 -  val add_classrel_i: (class * class) list -> sg -> sg
   1.147 +  val add_defsort: string -> theory -> theory
   1.148 +  val add_defsort_i: sort -> theory -> theory
   1.149 +  val add_types: (bstring * int * mixfix) list -> theory -> theory
   1.150 +  val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
   1.151 +  val add_nonterminals: bstring list -> theory -> theory
   1.152 +  val add_tyabbrs: (bstring * string list * string * mixfix) list -> theory -> theory
   1.153 +  val add_tyabbrs_i: (bstring * string list * typ * mixfix) list -> theory -> theory
   1.154 +  val add_arities: (xstring * string list * string) list -> theory -> theory
   1.155 +  val add_arities_i: (string * sort list * sort) list -> theory -> theory
   1.156 +  val add_syntax: (bstring * string * mixfix) list -> theory -> theory
   1.157 +  val add_syntax_i: (bstring * typ * mixfix) list -> theory -> theory
   1.158 +  val add_modesyntax: (string * bool) -> (bstring * string * mixfix) list -> theory -> theory
   1.159 +  val add_modesyntax_i: (string * bool) -> (bstring * typ * mixfix) list -> theory -> theory
   1.160 +  val del_modesyntax: (string * bool) -> (bstring * string * mixfix) list -> theory -> theory
   1.161 +  val del_modesyntax_i: (string * bool) -> (bstring * typ * mixfix) list -> theory -> theory
   1.162 +  val add_consts: (bstring * string * mixfix) list -> theory -> theory
   1.163 +  val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
   1.164 +  val add_classes: (bstring * xstring list) list -> theory -> theory
   1.165 +  val add_classes_i: (bstring * class list) list -> theory -> theory
   1.166 +  val add_classrel: (xstring * xstring) list -> theory -> theory
   1.167 +  val add_classrel_i: (class * class) list -> theory -> theory
   1.168    val add_trfuns:
   1.169      (string * (ast list -> ast)) list *
   1.170      (string * (term list -> term)) list *
   1.171      (string * (term list -> term)) list *
   1.172 -    (string * (ast list -> ast)) list -> sg -> sg
   1.173 +    (string * (ast list -> ast)) list -> theory -> theory
   1.174    val add_trfunsT:
   1.175 -    (string * (bool -> typ -> term list -> term)) list -> sg -> sg
   1.176 +    (string * (bool -> typ -> term list -> term)) list -> theory -> theory
   1.177    val add_advanced_trfuns:
   1.178 -    (string * (sg -> ast list -> ast)) list *
   1.179 -    (string * (sg -> term list -> term)) list *
   1.180 -    (string * (sg -> term list -> term)) list *
   1.181 -    (string * (sg -> ast list -> ast)) list -> sg -> sg
   1.182 +    (string * (theory -> ast list -> ast)) list *
   1.183 +    (string * (theory -> term list -> term)) list *
   1.184 +    (string * (theory -> term list -> term)) list *
   1.185 +    (string * (theory -> ast list -> ast)) list -> theory -> theory
   1.186    val add_advanced_trfunsT:
   1.187 -    (string * (sg -> bool -> typ -> term list -> term)) list -> sg -> sg
   1.188 +    (string * (theory -> bool -> typ -> term list -> term)) list -> theory -> theory
   1.189    val add_tokentrfuns:
   1.190 -    (string * string * (string -> string * real)) list -> sg -> sg
   1.191 -  val add_trrules: (xstring * string) Syntax.trrule list -> sg -> sg
   1.192 -  val add_trrules_i: ast Syntax.trrule list -> sg -> sg
   1.193 -  val add_path: string -> sg -> sg
   1.194 -  val qualified_names: sg -> sg
   1.195 -  val no_base_names: sg -> sg
   1.196 -  val custom_accesses: (string list -> string list list) -> sg -> sg
   1.197 -  val set_policy: (string -> bstring -> string) * (string list -> string list list) -> sg -> sg
   1.198 -  val restore_naming: sg -> sg -> sg
   1.199 -  val hide_classes: bool -> xstring list -> sg -> sg
   1.200 -  val hide_classes_i: bool -> string list -> sg -> sg
   1.201 -  val hide_types: bool -> xstring list -> sg -> sg
   1.202 -  val hide_types_i: bool -> string list -> sg -> sg
   1.203 -  val hide_consts: bool -> xstring list -> sg -> sg
   1.204 -  val hide_consts_i: bool -> string list -> sg -> sg
   1.205 -  val merge_refs: sg_ref * sg_ref -> sg_ref
   1.206 -  val merge: sg * sg -> sg
   1.207 -  val prep_ext_merge: sg list -> sg
   1.208 -end;
   1.209 +    (string * string * (string -> string * real)) list -> theory -> theory
   1.210 +  val add_mode_tokentrfuns: string -> (string * (string -> string * real)) list
   1.211 +    -> theory -> theory
   1.212 +  val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
   1.213 +  val add_trrules_i: ast Syntax.trrule list -> theory -> theory
   1.214 +  val add_path: string -> theory -> theory
   1.215 +  val parent_path: theory -> theory
   1.216 +  val root_path: theory -> theory
   1.217 +  val absolute_path: theory -> theory
   1.218 +  val local_path: theory -> theory
   1.219 +  val qualified_names: theory -> theory
   1.220 +  val no_base_names: theory -> theory
   1.221 +  val custom_accesses: (string list -> string list list) -> theory -> theory
   1.222 +  val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
   1.223 +    theory -> theory
   1.224 +  val restore_naming: theory -> theory -> theory
   1.225 +  val hide_classes: bool -> xstring list -> theory -> theory
   1.226 +  val hide_classes_i: bool -> string list -> theory -> theory
   1.227 +  val hide_types: bool -> xstring list -> theory -> theory
   1.228 +  val hide_types_i: bool -> string list -> theory -> theory
   1.229 +  val hide_consts: bool -> xstring list -> theory -> theory
   1.230 +  val hide_consts_i: bool -> string list -> theory -> theory
   1.231 +end
   1.232  
   1.233 -signature PRIVATE_SIGN =
   1.234 +signature SIGN =
   1.235  sig
   1.236 -  include SIGN
   1.237 -  val init_data: Object.kind * (Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) *
   1.238 -    (Object.T * Object.T -> Object.T) * (sg -> Object.T -> unit)) -> sg -> sg
   1.239 -  val get_data: Object.kind -> (Object.T -> 'a) -> sg -> 'a
   1.240 -  val put_data: Object.kind -> ('a -> Object.T) -> 'a -> sg -> sg
   1.241 -  val print_data: Object.kind -> sg -> unit
   1.242 -end;
   1.243 +  type syn
   1.244 +  type sg    (*obsolete*)
   1.245 +  val init: theory -> theory
   1.246 +  val rep_sg: theory ->
   1.247 +   {naming: NameSpace.naming,
   1.248 +    syn: syn,
   1.249 +    tsig: Type.tsig,
   1.250 +    consts: (typ * stamp) NameSpace.table}
   1.251 +  val naming_of: theory -> NameSpace.naming
   1.252 +  val base_name: string -> bstring
   1.253 +  val full_name: theory -> bstring -> string
   1.254 +  val full_name_path: theory -> string -> bstring -> string
   1.255 +  val declare_name: theory -> string -> NameSpace.T -> NameSpace.T
   1.256 +  val syn_of: theory -> Syntax.syntax
   1.257 +  val tsig_of: theory -> Type.tsig
   1.258 +  val classes: theory -> class list
   1.259 +  val defaultS: theory -> sort
   1.260 +  val subsort: theory -> sort * sort -> bool
   1.261 +  val of_sort: theory -> typ * sort -> bool
   1.262 +  val witness_sorts: theory -> sort list -> sort list -> (typ * sort) list
   1.263 +  val universal_witness: theory -> (typ * sort) option
   1.264 +  val typ_instance: theory -> typ * typ -> bool
   1.265 +  val is_logtype: theory -> string -> bool
   1.266 +  val const_type: theory -> string -> typ option
   1.267 +  val the_const_type: theory -> string -> typ
   1.268 +  val declared_tyname: theory -> string -> bool
   1.269 +  val declared_const: theory -> string -> bool
   1.270 +  val class_space: theory -> NameSpace.T
   1.271 +  val type_space: theory -> NameSpace.T
   1.272 +  val const_space: theory -> NameSpace.T
   1.273 +  val intern_class: theory -> xstring -> string
   1.274 +  val extern_class: theory -> string -> xstring
   1.275 +  val intern_type: theory -> xstring -> string
   1.276 +  val extern_type: theory -> string -> xstring
   1.277 +  val intern_const: theory -> xstring -> string
   1.278 +  val extern_const: theory -> string -> xstring
   1.279 +  val intern_sort: theory -> sort -> sort
   1.280 +  val extern_sort: theory -> sort -> sort
   1.281 +  val intern_typ: theory -> typ -> typ
   1.282 +  val extern_typ: theory -> typ -> typ
   1.283 +  val intern_term: theory -> term -> term
   1.284 +  val extern_term: theory -> term -> term
   1.285 +  val intern_tycons: theory -> typ -> typ
   1.286 +  val pretty_term': Syntax.syntax -> theory -> term -> Pretty.T
   1.287 +  val pretty_term: theory -> term -> Pretty.T
   1.288 +  val pretty_typ: theory -> typ -> Pretty.T
   1.289 +  val pretty_sort: theory -> sort -> Pretty.T
   1.290 +  val pretty_classrel: theory -> class list -> Pretty.T
   1.291 +  val pretty_arity: theory -> arity -> Pretty.T
   1.292 +  val string_of_term: theory -> term -> string
   1.293 +  val string_of_typ: theory -> typ -> string
   1.294 +  val string_of_sort: theory -> sort -> string
   1.295 +  val string_of_classrel: theory -> class list -> string
   1.296 +  val string_of_arity: theory -> arity -> string
   1.297 +  val pprint_term: theory -> term -> pprint_args -> unit
   1.298 +  val pprint_typ: theory -> typ -> pprint_args -> unit
   1.299 +  val pp: theory -> Pretty.pp
   1.300 +  val certify_class: theory -> class -> class
   1.301 +  val certify_sort: theory -> sort -> sort
   1.302 +  val certify_typ: theory -> typ -> typ
   1.303 +  val certify_typ_syntax: theory -> typ -> typ
   1.304 +  val certify_typ_abbrev: theory -> typ -> typ
   1.305 +  val certify_term: Pretty.pp -> theory -> term -> term * typ * int
   1.306 +  val read_sort': Syntax.syntax -> theory -> string -> sort
   1.307 +  val read_sort: theory -> string -> sort
   1.308 +  val read_typ': Syntax.syntax -> theory * (indexname -> sort option) -> string -> typ
   1.309 +  val read_typ_syntax': Syntax.syntax -> theory * (indexname -> sort option) -> string -> typ
   1.310 +  val read_typ_abbrev': Syntax.syntax -> theory * (indexname -> sort option) -> string -> typ
   1.311 +  val read_typ: theory * (indexname -> sort option) -> string -> typ
   1.312 +  val read_typ_syntax: theory * (indexname -> sort option) -> string -> typ
   1.313 +  val read_typ_abbrev: theory * (indexname -> sort option) -> string -> typ
   1.314 +  val read_tyname: theory -> string -> typ
   1.315 +  val read_const: theory -> string -> term
   1.316 +  val infer_types_simult: Pretty.pp -> theory -> (indexname -> typ option) ->
   1.317 +    (indexname -> sort option) -> string list -> bool
   1.318 +    -> (term list * typ) list -> term list * (indexname * typ) list
   1.319 +  val infer_types: Pretty.pp -> theory -> (indexname -> typ option) ->
   1.320 +    (indexname -> sort option) -> string list -> bool
   1.321 +    -> term list * typ -> term * (indexname * typ) list
   1.322 +  val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax ->
   1.323 +    theory * (indexname -> typ option) * (indexname -> sort option) ->
   1.324 +    string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
   1.325 +  val read_def_terms:
   1.326 +    theory * (indexname -> typ option) * (indexname -> sort option) ->
   1.327 +    string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
   1.328 +  val simple_read_term: theory -> typ -> string -> term
   1.329 +  val const_of_class: class -> string
   1.330 +  val class_of_const: string -> class
   1.331 +  include SIGN_THEORY
   1.332 +end
   1.333  
   1.334 -structure Sign: PRIVATE_SIGN =
   1.335 +structure Sign: SIGN =
   1.336  struct
   1.337  
   1.338 -(** datatype sg **)
   1.339 -
   1.340 -(* types sg, data, syn, sg_ref *)
   1.341 -
   1.342 -datatype sg =
   1.343 -  Sg of
   1.344 -   {id: string ref,
   1.345 -    stamps: string ref list,                  (*unique theory indentifier*)
   1.346 -    syn: syn} *                               (*syntax for parsing and printing*)
   1.347 -   {self: sg_ref,                             (*mutable self reference*)
   1.348 -    tsig: Type.tsig,                          (*order-sorted signature of types*)
   1.349 -    consts: (typ * stamp) NameSpace.table,    (*type schemes of constants*)
   1.350 -    naming: NameSpace.naming,
   1.351 -    data: data}
   1.352 -and data =
   1.353 -  Data of
   1.354 -    (Object.kind *                                (*kind (for authorization)*)
   1.355 -      (Object.T *                                 (*value*)
   1.356 -        ((Object.T -> Object.T) *                 (*copy method*)
   1.357 -          (Object.T -> Object.T) *                (*prepare extend method*)
   1.358 -          (Object.T * Object.T -> Object.T) *     (*merge and prepare extend method*)
   1.359 -          (sg -> Object.T -> unit))))             (*print method*)
   1.360 -    Symtab.table
   1.361 -and syn =
   1.362 -  Syn of
   1.363 -    Syntax.syntax *
   1.364 -     (((sg -> ast list -> ast) * stamp) Symtab.table *
   1.365 -      ((sg -> term list -> term) * stamp) Symtab.table *
   1.366 -      ((sg -> bool -> typ -> term list -> term) * stamp) list Symtab.table *
   1.367 -      ((sg -> ast list -> ast) * stamp) list Symtab.table)
   1.368 -and sg_ref =
   1.369 -  SgRef of sg ref option;
   1.370 -
   1.371 -(* FIXME assign!??? *)
   1.372 -fun make_sg (id, self, stamps) naming data (syn, tsig, consts) =
   1.373 -  Sg ({id = id, stamps = stamps, syn = syn}, {self = self, tsig = tsig,
   1.374 -    consts = consts, naming = naming, data = data});
   1.375 -
   1.376 -fun rep_sg (Sg (_, args)) = args;
   1.377 -
   1.378 -
   1.379 -(* stamps *)
   1.380 -
   1.381 -fun stamps_of (Sg ({stamps, ...}, _)) = stamps;
   1.382 -val stamp_names_of = rev o map ! o stamps_of;
   1.383 -fun exists_stamp name = exists (equal name o !) o stamps_of;
   1.384 -
   1.385 -fun is_stale (Sg ({id, ...}, {self = SgRef (SOME (ref (Sg ({id = id', ...}, _)))), ...})) =
   1.386 -      id <> id'
   1.387 -  | is_stale _ = false;
   1.388 -
   1.389 -fun pretty_sg sg =
   1.390 -  Pretty.str_list "{" "}" (stamp_names_of sg @ (if is_stale sg then ["!"] else []));
   1.391 -
   1.392 -val pprint_sg = Pretty.pprint o pretty_sg;
   1.393 -
   1.394 -fun pretty_abbrev_sg sg =
   1.395 -  let
   1.396 -    val stamps = map ! (stamps_of sg);
   1.397 -    val abbrev = if length stamps > 5 then "..." :: rev (List.take (stamps, 5)) else rev stamps;
   1.398 -  in Pretty.str_list "{" "}" abbrev end;
   1.399 -
   1.400 -val str_of_sg = Pretty.str_of o pretty_abbrev_sg;
   1.401 -
   1.402 -
   1.403 -(* id and self *)
   1.404 -
   1.405 -fun check_stale pos sg =
   1.406 -  if is_stale sg then raise TERM ("Stale signature (in " ^ pos ^ "): " ^ str_of_sg sg, [])
   1.407 -  else sg;
   1.408 -
   1.409 -fun self_ref (sg as Sg (_, {self, ...})) = (check_stale "Sign.self_ref" sg; self);
   1.410 -
   1.411 -fun deref (SgRef (SOME (ref sg))) = sg
   1.412 -  | deref (SgRef NONE) = sys_error "Sign.deref";
   1.413 -
   1.414 -fun assign (SgRef (SOME r)) sg = r := sg
   1.415 -  | assign (SgRef NONE) _ = sys_error "Sign.assign";
   1.416 -
   1.417 -fun name_of (sg as Sg ({id = ref name, ...}, _)) =
   1.418 -  if name = "" orelse ord name = ord "#" then
   1.419 -    raise TERM ("Nameless signature " ^ str_of_sg sg, [])
   1.420 -  else name;
   1.421 -
   1.422 -fun is_draft (Sg ({stamps = ref name :: _, ...}, _)) =
   1.423 -      name = "" orelse ord name = ord "#"
   1.424 -  | is_draft _ = sys_error "Sign.is_draft";
   1.425 -
   1.426 -
   1.427 -(* inclusion and equality *)
   1.428 -
   1.429 -local
   1.430 -  (*avoiding polymorphic equality: factor 10 speedup*)
   1.431 -  fun mem_stamp (_: string ref, []) = false
   1.432 -    | mem_stamp (x, y :: ys) = x = y orelse mem_stamp (x, ys);
   1.433 -
   1.434 -  fun subset_stamp ([], ys) = true
   1.435 -    | subset_stamp (x :: xs, ys) =
   1.436 -        mem_stamp (x, ys) andalso subset_stamp (xs, ys);
   1.437 -in
   1.438 -  fun eq_sg (sg1 as Sg ({id = id1, ...}, _), sg2 as Sg ({id = id2, ...}, _)) =
   1.439 -    (check_stale "Sign.eq_sg" sg1; check_stale "Sign.eq_sg" sg2; id1 = id2);
   1.440 -
   1.441 -  fun subsig (sg1, sg2) =
   1.442 -    eq_sg (sg1, sg2) orelse mem_stamp (hd (stamps_of sg1), stamps_of sg2);
   1.443 -
   1.444 -  fun subsig_internal (sg1, sg2) =
   1.445 -    eq_sg (sg1, sg2) orelse subset_stamp (stamps_of sg1, stamps_of sg2);
   1.446 -end;
   1.447 +type sg = theory;
   1.448  
   1.449  
   1.450 -fun joinable (sg1, sg2) = subsig (sg1, sg2) orelse subsig (sg2, sg1);
   1.451 -
   1.452 -(*test if same theory names are contained in signatures' stamps,
   1.453 -  i.e. if signatures belong to same theory but not necessarily to the
   1.454 -  same version of it*)
   1.455 -fun same_sg (sg1, sg2) =
   1.456 -  eq_sg (sg1, sg2) orelse eq_set_string (pairself (map ! o stamps_of) (sg1, sg2));
   1.457 -
   1.458 -
   1.459 -(* data operations *)
   1.460 -
   1.461 -fun err_method name kind e =    (* FIXME wrap exn msg!? *)
   1.462 -  (warning ("Error while invoking " ^ quote kind ^ " " ^ name ^ " method"); raise e);
   1.463 -
   1.464 -fun err_inconsistent kinds =
   1.465 -  error ("Attempt to merge different versions of " ^ commas_quote kinds ^ " data");
   1.466 -
   1.467 -val empty_data = Data Symtab.empty;
   1.468 -
   1.469 -fun merge_data (Data tab1, Data tab2) =
   1.470 -  let
   1.471 -    val data1 = map snd (Symtab.dest tab1);
   1.472 -    val data2 = map snd (Symtab.dest tab2);
   1.473 -    val all_data = data1 @ data2;
   1.474 -    val kinds = gen_distinct Object.eq_kind (map fst all_data);
   1.475 -
   1.476 -   fun entry data kind =
   1.477 -     (case gen_assoc Object.eq_kind (data, kind) of
   1.478 -       NONE => []
   1.479 -     | SOME x => [(kind, x)]);
   1.480 -
   1.481 -    fun merge_entries [(kind, (e, mths as (_, ext, _, _)))] =
   1.482 -          (kind, (ext e handle exn => err_method "prep_ext" (Object.name_of_kind kind) exn, mths))
   1.483 -      | merge_entries [(kind, (e1, mths as (_, _, mrg, _))), (_, (e2, _))] =
   1.484 -          (kind, (mrg (e1, e2)
   1.485 -            handle exn => err_method "merge" (Object.name_of_kind kind) exn, mths))
   1.486 -      | merge_entries _ = sys_error "merge_entries";
   1.487 -
   1.488 -    val data = map (fn k => merge_entries (entry data1 k @ entry data2 k)) kinds;
   1.489 -    val data_idx = map (fn (k, x) => (Object.name_of_kind k, (k, x))) data;
   1.490 -  in
   1.491 -    Data (Symtab.make data_idx)
   1.492 -      handle Symtab.DUPS dups => err_inconsistent dups
   1.493 -  end;
   1.494 -
   1.495 -fun prep_ext_data data = merge_data (data, empty_data);
   1.496 -
   1.497 -fun copy_data (Data tab) =
   1.498 -  let
   1.499 -    fun cp_data (k, (e, mths as (cp, _, _, _))) =
   1.500 -      (k, (cp e handle exn => err_method "copy" (Object.name_of_kind k) exn, mths));
   1.501 -  in Data (Symtab.map cp_data tab) end;
   1.502 -
   1.503 -
   1.504 -
   1.505 -(** build signatures **)
   1.506 -
   1.507 -fun create_sg name self stamps naming data sign =
   1.508 -  let
   1.509 -    val id = ref name;
   1.510 -    val stamps' = (case stamps of ref "#" :: ss => ss | ss => ss);
   1.511 -    val _ = conditional (exists (equal name o !) stamps')
   1.512 -      (fn () => error ("Theory already contains a " ^ quote name ^ " component"));
   1.513 -    val sg = make_sg (id, self, id :: stamps') naming data sign;
   1.514 -  in assign self sg; sg end;
   1.515 -
   1.516 -fun new_sg f (sg as Sg ({stamps, syn, ...}, {self = _, tsig, consts, naming, data})) =
   1.517 -  let
   1.518 -    val _ = check_stale "Sign.new_sg" sg;
   1.519 -    val self' = SgRef (SOME (ref sg));
   1.520 -    val data' = f data;
   1.521 -  in create_sg "#" self' stamps naming data' (syn, tsig, consts) end;
   1.522 -
   1.523 -val prep_ext = new_sg prep_ext_data;
   1.524 -val copy = new_sg copy_data;
   1.525 +(** datatype syn **)    (* FIXME use Syntax.syntax here (include advanced trfuns there) *)
   1.526  
   1.527 -fun add_name name (sg as Sg ({stamps, syn, ...}, {self, tsig, consts, naming, data})) =
   1.528 -  let
   1.529 -    val _ = check_stale "Sign.add_name" sg;
   1.530 -    val (self', data') =
   1.531 -      if is_draft sg then (self, data)
   1.532 -      else (SgRef (SOME (ref sg)), prep_ext_data data);
   1.533 -  in create_sg name self' stamps naming data' (syn, tsig, consts) end;
   1.534 -
   1.535 -fun map_sg keep f (sg as Sg ({stamps, syn, ...}, {self, tsig, consts, naming, data})) =
   1.536 -  let
   1.537 -    val _ = check_stale "Sign.map_sg" sg;
   1.538 -    val (self', data') =
   1.539 -      if is_draft sg andalso keep then (self, data)
   1.540 -      else (SgRef (SOME (ref sg)), prep_ext_data data);
   1.541 -    val (naming', data', sign') = f (naming, data', (syn, tsig, consts));
   1.542 -  in create_sg "#" self' stamps naming' data' sign' end;
   1.543 -
   1.544 -fun map_naming f = map_sg true (fn (naming, data, sign) => (f naming, data, sign));
   1.545 -fun map_data f = map_sg true (fn (naming, data, sign) => (naming, f data, sign));
   1.546 -fun map_sign f = map_sg true (fn (naming, data, sign) => (naming, data, f sign));
   1.547 -fun map_syn f = map_sign (fn (syn, tsig, consts) => (f syn, tsig, consts));
   1.548 -fun map_tsig f = map_sign (fn (syn, tsig, consts) => (syn, f tsig, consts));
   1.549 -fun map_consts f = map_sign (fn (syn, tsig, consts) => (syn, tsig, f consts));
   1.550 -
   1.551 -
   1.552 -
   1.553 -(** signature data **)
   1.554 -
   1.555 -(* errors *)
   1.556 -
   1.557 -fun of_theory sg = "\nof theory " ^ str_of_sg sg;
   1.558 -
   1.559 -fun err_dup_init sg kind =
   1.560 -  error ("Duplicate initialization of " ^ quote kind ^ " data" ^ of_theory sg);
   1.561 -
   1.562 -fun err_uninit sg kind =
   1.563 -  error ("Tried to access uninitialized " ^ quote kind ^ " data" ^ of_theory sg);
   1.564 +datatype syn =
   1.565 +  Syn of
   1.566 +    Syntax.syntax *
   1.567 +     (((theory -> ast list -> ast) * stamp) Symtab.table *
   1.568 +      ((theory -> term list -> term) * stamp) Symtab.table *
   1.569 +      ((theory -> bool -> typ -> term list -> term) * stamp) list Symtab.table *
   1.570 +      ((theory -> ast list -> ast) * stamp) list Symtab.table)
   1.571  
   1.572 -fun err_access sg kind =
   1.573 -  error ("Unauthorized access to " ^ quote kind ^ " data" ^ of_theory sg);
   1.574 -
   1.575 -
   1.576 -(* access data *)
   1.577 -
   1.578 -fun data_kinds (Data tab) = Symtab.keys tab;
   1.579 -
   1.580 -fun lookup_data sg tab kind =
   1.581 -  let val name = Object.name_of_kind kind in
   1.582 -    (case Symtab.lookup (tab, name) of
   1.583 -      SOME (k, x) =>
   1.584 -        if Object.eq_kind (kind, k) then x
   1.585 -        else err_access sg name
   1.586 -    | NONE => err_uninit sg name)
   1.587 -  end;
   1.588 -
   1.589 -fun init_data (kind, (e, cp, ext, mrg, prt)) sg = sg |> map_data (fn Data tab =>
   1.590 -  Data (Symtab.update_new ((Object.name_of_kind kind, (kind, (e, (cp, ext, mrg, prt)))), tab))
   1.591 -    handle Symtab.DUP name => err_dup_init sg name);
   1.592 -
   1.593 -fun get_data kind dest (sg as Sg (_, {data = Data tab, ...})) =
   1.594 -  let val x = fst (lookup_data sg tab kind)
   1.595 -  in dest x handle Match => Object.kind_error kind end;
   1.596 -
   1.597 -fun put_data kind mk x sg = sg |> map_data (fn Data tab =>
   1.598 -  Data (Symtab.update ((Object.name_of_kind kind,
   1.599 -    (kind, (mk x, snd (lookup_data sg tab kind)))), tab)));
   1.600 -
   1.601 -fun print_data kind (sg as Sg (_, {data = Data tab, ...})) =
   1.602 -  let val (e, (_, _, _, prt)) = lookup_data sg tab kind in
   1.603 -    prt sg e handle exn =>
   1.604 -      err_method ("print" ^ of_theory sg) (Object.name_of_kind kind) exn
   1.605 -  end;
   1.606 -
   1.607 -fun print_all_data (sg as Sg (_, {data = Data tab, ...})) =
   1.608 -  List.app (fn kind => print_data kind sg) (map (#1 o #2) (Symtab.dest tab));
   1.609 -
   1.610 -
   1.611 -
   1.612 -(** primitive signatures **)
   1.613 +fun merge_trfuns
   1.614 +    (parse_ast_trtab1, parse_trtab1, print_trtab1, print_ast_trtab1)
   1.615 +    (parse_ast_trtab2, parse_trtab2, print_trtab2, print_ast_trtab2) =
   1.616 +  (Syntax.merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2,
   1.617 +    Syntax.merge_trtabs "parse translation" parse_trtab1 parse_trtab2,
   1.618 +    Syntax.merge_tr'tabs print_trtab1 print_trtab2,
   1.619 +    Syntax.merge_tr'tabs print_ast_trtab1 print_ast_trtab2);
   1.620  
   1.621  val pure_syn =
   1.622    Syn (Syntax.pure_syn, (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty));
   1.623  
   1.624 -val dummy_sg = make_sg (ref "", SgRef NONE, []) NameSpace.default_naming empty_data
   1.625 -  (pure_syn, Type.empty_tsig, NameSpace.empty_table);
   1.626 -
   1.627 -val pre_pure =
   1.628 -  create_sg "#" (SgRef (SOME (ref dummy_sg))) [] NameSpace.default_naming empty_data
   1.629 -    (pure_syn, Type.empty_tsig, NameSpace.empty_table);
   1.630 -
   1.631 -val PureN = "Pure";
   1.632 -val CPureN = "CPure";
   1.633  
   1.634  
   1.635 +(** datatype sign **)
   1.636  
   1.637 -(** signature content **)
   1.638 +datatype sign = Sign of
   1.639 + {naming: NameSpace.naming,                 (*common naming conventions*)
   1.640 +  syn: syn,                                 (*concrete syntax for terms, types, sorts*)
   1.641 +  tsig: Type.tsig,                          (*order-sorted signature of types*)
   1.642 +  consts: (typ * stamp) NameSpace.table};   (*type schemes of term constants*)
   1.643 +
   1.644 +fun make_sign (naming, syn, tsig, consts) =
   1.645 +  Sign {naming = naming, syn = syn, tsig = tsig, consts = consts};
   1.646 +
   1.647 +fun err_dup_consts cs =
   1.648 +  error ("Duplicate declaration of constant(s) " ^ commas_quote cs);
   1.649 +
   1.650 +structure SignData = TheoryDataFun
   1.651 +(struct
   1.652 +  val name = "Pure/sign";
   1.653 +  type T = sign;
   1.654 +  val copy = I;
   1.655 +  val extend = I;
   1.656 +
   1.657 +  val empty =
   1.658 +    make_sign (NameSpace.default_naming, pure_syn, Type.empty_tsig, NameSpace.empty_table);
   1.659 +
   1.660 +  fun merge pp (sign1, sign2) =
   1.661 +    let
   1.662 +      val Sign {naming = _, syn = Syn (syntax1, trfuns1), tsig = tsig1,
   1.663 +        consts = consts1} = sign1;
   1.664 +      val Sign {naming = _, syn = Syn (syntax2, trfuns2), tsig = tsig2,
   1.665 +        consts = consts2} = sign2;
   1.666 +
   1.667 +      val naming = NameSpace.default_naming;
   1.668 +      val syntax = Syntax.merge_syntaxes syntax1 syntax2;
   1.669 +      val trfuns = merge_trfuns trfuns1 trfuns2;
   1.670 +      val syn = Syn (syntax, trfuns);
   1.671 +      val tsig = Type.merge_tsigs pp (tsig1, tsig2);
   1.672 +      val consts = NameSpace.merge_tables eq_snd (consts1, consts2)
   1.673 +        handle Symtab.DUPS cs => err_dup_consts cs;
   1.674 +    in make_sign (naming, syn, tsig, consts) end;
   1.675 +
   1.676 +  fun print _ _ = ();
   1.677 +end);
   1.678 +
   1.679 +val init = SignData.init;
   1.680 +
   1.681 +fun rep_sg thy = SignData.get thy |> (fn Sign args => args);
   1.682 +
   1.683 +fun map_sign f = SignData.map (fn Sign {naming, syn, tsig, consts} =>
   1.684 +  make_sign (f (naming, syn, tsig, consts)));
   1.685 +
   1.686 +fun map_naming f = map_sign (fn (naming, syn, tsig, consts) => (f naming, syn, tsig, consts));
   1.687 +fun map_syn f = map_sign (fn (naming, syn, tsig, consts) => (naming, f syn, tsig, consts));
   1.688 +fun map_tsig f = map_sign (fn (naming, syn, tsig, consts) => (naming, syn, f tsig, consts));
   1.689 +fun map_consts f = map_sign (fn (naming, syn, tsig, consts) => (naming, syn, tsig, f consts));
   1.690 +
   1.691  
   1.692  (* naming *)
   1.693  
   1.694 -fun naming_of (Sg (_, {naming, ...})) = naming;
   1.695 -
   1.696 +val naming_of = #naming o rep_sg;
   1.697  val base_name = NameSpace.base;
   1.698  val full_name = NameSpace.full o naming_of;
   1.699 -fun full_name_path sg elems = NameSpace.full (NameSpace.add_path elems (naming_of sg));
   1.700 +fun full_name_path thy elems = NameSpace.full (NameSpace.add_path elems (naming_of thy));
   1.701  val declare_name = NameSpace.declare o naming_of;
   1.702  
   1.703  
   1.704 @@ -485,14 +259,14 @@
   1.705  
   1.706  fun map_syntax f (Syn (syntax, trfuns)) = Syn (f syntax, trfuns);
   1.707  
   1.708 -fun make_syntax sg (Syn (syntax, (atrs, trs, tr's, atr's))) =
   1.709 +fun make_syntax thy (Syn (syntax, (atrs, trs, tr's, atr's))) =
   1.710    let
   1.711 -    fun apply (c, (f, s)) = (c, (f sg, s));
   1.712 +    fun apply (c, (f, s)) = (c, (f thy, s));
   1.713      fun prep tab = map apply (Symtab.dest tab);
   1.714      fun prep' tab = map apply (Symtab.dest_multi tab);
   1.715    in syntax |> Syntax.extend_trfuns (prep atrs, prep trs, prep' tr's, prep' atr's) end;
   1.716  
   1.717 -fun syn_of (sg as Sg ({syn, ...}, _)) = make_syntax sg syn;
   1.718 +fun syn_of thy = make_syntax thy (#syn (rep_sg thy));
   1.719  
   1.720  
   1.721  (* advanced translation functions *)
   1.722 @@ -504,19 +278,10 @@
   1.723      Syntax.extend_tr'tab tr's print_trtab,
   1.724      Syntax.extend_tr'tab atr's print_ast_trtab));
   1.725  
   1.726 -fun merge_trfuns
   1.727 -    (parse_ast_trtab1, parse_trtab1, print_trtab1, print_ast_trtab1)
   1.728 -    (parse_ast_trtab2, parse_trtab2, print_trtab2, print_ast_trtab2) =
   1.729 -  (Syntax.merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2,
   1.730 -    Syntax.merge_trtabs "parse translation" parse_trtab1 parse_trtab2,
   1.731 -    Syntax.merge_tr'tabs print_trtab1 print_trtab2,
   1.732 -    Syntax.merge_tr'tabs print_ast_trtab1 print_ast_trtab2);
   1.733 -
   1.734  
   1.735  (* type signature *)
   1.736  
   1.737  val tsig_of = #tsig o rep_sg;
   1.738 -
   1.739  val classes = Type.classes o tsig_of;
   1.740  val defaultS = Type.defaultS o tsig_of;
   1.741  val subsort = Type.subsort o tsig_of;
   1.742 @@ -524,21 +289,21 @@
   1.743  val witness_sorts = Type.witness_sorts o tsig_of;
   1.744  val universal_witness = Type.universal_witness o tsig_of;
   1.745  val typ_instance = Type.typ_instance o tsig_of;
   1.746 -fun is_logtype sg c = c mem_string Type.logical_types (tsig_of sg);
   1.747 +fun is_logtype thy c = c mem_string Type.logical_types (tsig_of thy);
   1.748  
   1.749  
   1.750  (* consts signature *)
   1.751  
   1.752 -fun const_type (Sg (_, {consts, ...})) c = Option.map #1 (Symtab.lookup (#2 consts, c));
   1.753 +fun const_type thy c = Option.map #1 (Symtab.lookup (#2 (#consts (rep_sg thy)), c));
   1.754  
   1.755 -fun the_const_type sg c =
   1.756 -  (case const_type sg c of SOME T => T
   1.757 +fun the_const_type thy c =
   1.758 +  (case const_type thy c of SOME T => T
   1.759    | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
   1.760  
   1.761 -fun declared_tyname sg c =
   1.762 -  is_some (Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of sg))), c));
   1.763 +fun declared_tyname thy c =
   1.764 +  is_some (Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of thy))), c));
   1.765  
   1.766 -fun declared_const sg c = is_some (const_type sg c);
   1.767 +val declared_const = is_some oo const_type;
   1.768  
   1.769  
   1.770  
   1.771 @@ -567,16 +332,16 @@
   1.772      fun get x = if_none (assoc_string (tab, x)) x;
   1.773    in get end;
   1.774  
   1.775 -fun typ_mapping f g sg T =
   1.776 +fun typ_mapping f g thy T =
   1.777    T |> Term.map_typ
   1.778 -    (mapping add_typ_classes (f sg) T)
   1.779 -    (mapping add_typ_tycons (g sg) T);
   1.780 +    (mapping add_typ_classes (f thy) T)
   1.781 +    (mapping add_typ_tycons (g thy) T);
   1.782  
   1.783 -fun term_mapping f g h sg t =
   1.784 +fun term_mapping f g h thy t =
   1.785    t |> Term.map_term
   1.786 -    (mapping add_term_classes (f sg) t)
   1.787 -    (mapping add_term_tycons (g sg) t)
   1.788 -    (mapping add_term_consts (h sg) t);
   1.789 +    (mapping add_term_classes (f thy) t)
   1.790 +    (mapping add_term_tycons (g thy) t)
   1.791 +    (mapping add_term_consts (h thy) t);
   1.792  
   1.793  in
   1.794  
   1.795 @@ -592,21 +357,22 @@
   1.796  
   1.797  (** pretty printing of terms, types etc. **)
   1.798  
   1.799 -fun pretty_term' syn sg t = Syntax.pretty_term syn (exists_stamp CPureN sg) (extern_term sg t);
   1.800 -fun pretty_term sg t = pretty_term' (syn_of sg) sg t;
   1.801 -fun pretty_typ sg T = Syntax.pretty_typ (syn_of sg) (extern_typ sg T);
   1.802 -fun pretty_sort sg S = Syntax.pretty_sort (syn_of sg) (extern_sort sg S);
   1.803 +fun pretty_term' syn thy t =
   1.804 +  Syntax.pretty_term syn (Context.exists_name Context.CPureN thy) (extern_term thy t);
   1.805 +fun pretty_term thy t = pretty_term' (syn_of thy) thy t;
   1.806 +fun pretty_typ thy T = Syntax.pretty_typ (syn_of thy) (extern_typ thy T);
   1.807 +fun pretty_sort thy S = Syntax.pretty_sort (syn_of thy) (extern_sort thy S);
   1.808  
   1.809 -fun pretty_classrel sg cs = Pretty.block (List.concat
   1.810 -  (separate [Pretty.str " <", Pretty.brk 1] (map (single o pretty_sort sg o single) cs)));
   1.811 +fun pretty_classrel thy cs = Pretty.block (List.concat
   1.812 +  (separate [Pretty.str " <", Pretty.brk 1] (map (single o pretty_sort thy o single) cs)));
   1.813  
   1.814 -fun pretty_arity sg (a, Ss, S) =
   1.815 +fun pretty_arity thy (a, Ss, S) =
   1.816    let
   1.817 -    val a' = extern_type sg a;
   1.818 +    val a' = extern_type thy a;
   1.819      val dom =
   1.820        if null Ss then []
   1.821 -      else [Pretty.list "(" ")" (map (pretty_sort sg) Ss), Pretty.brk 1];
   1.822 -  in Pretty.block ([Pretty.str (a' ^ " ::"), Pretty.brk 1] @ dom @ [pretty_sort sg S]) end;
   1.823 +      else [Pretty.list "(" ")" (map (pretty_sort thy) Ss), Pretty.brk 1];
   1.824 +  in Pretty.block ([Pretty.str (a' ^ " ::"), Pretty.brk 1] @ dom @ [pretty_sort thy S]) end;
   1.825  
   1.826  val string_of_term = Pretty.string_of oo pretty_term;
   1.827  val string_of_typ = Pretty.string_of oo pretty_typ;
   1.828 @@ -617,8 +383,8 @@
   1.829  val pprint_term = (Pretty.pprint o Pretty.quote) oo pretty_term;
   1.830  val pprint_typ = (Pretty.pprint o Pretty.quote) oo pretty_typ;
   1.831  
   1.832 -fun pp sg = Pretty.pp (pretty_term sg, pretty_typ sg, pretty_sort sg,
   1.833 -  pretty_classrel sg, pretty_arity sg);
   1.834 +fun pp thy = Pretty.pp (pretty_term thy, pretty_typ thy, pretty_sort thy,
   1.835 +  pretty_classrel thy, pretty_arity thy);
   1.836  
   1.837  
   1.838  
   1.839 @@ -626,7 +392,7 @@
   1.840  
   1.841  (* certify wrt. type signature *)
   1.842  
   1.843 -fun certify cert = cert o tsig_of o check_stale "Sign.certify";
   1.844 +fun certify cert = cert o tsig_of o Context.check_thy "Sign.certify";
   1.845  
   1.846  val certify_class      = certify Type.cert_class;
   1.847  val certify_sort       = certify Type.cert_sort;
   1.848 @@ -669,11 +435,11 @@
   1.849  
   1.850  in
   1.851  
   1.852 -fun certify_term pp sg tm =
   1.853 +fun certify_term pp thy tm =
   1.854    let
   1.855 -    val _ = check_stale "Sign.certify_term" sg;
   1.856 +    val _ = Context.check_thy "Sign.certify_term" thy;
   1.857  
   1.858 -    val tm' = map_term_types (Type.cert_typ (tsig_of sg)) tm;
   1.859 +    val tm' = map_term_types (certify_typ thy) tm;
   1.860      val tm' = if tm = tm' then tm else tm';  (*avoid copying of already normal term*)
   1.861  
   1.862      fun err msg = raise TYPE (msg, [], [tm']);
   1.863 @@ -683,10 +449,10 @@
   1.864      fun check_atoms (t $ u) = (check_atoms t; check_atoms u)
   1.865        | check_atoms (Abs (_, _, t)) = check_atoms t
   1.866        | check_atoms (Const (a, T)) =
   1.867 -          (case const_type sg a of
   1.868 +          (case const_type thy a of
   1.869              NONE => err ("Undeclared constant " ^ show_const a T)
   1.870            | SOME U =>
   1.871 -              if typ_instance sg (T, U) then ()
   1.872 +              if typ_instance thy (T, U) then ()
   1.873                else err ("Illegal type for constant " ^ show_const a T))
   1.874        | check_atoms (Var ((x, i), _)) =
   1.875            if i < 0 then err ("Malformed variable: " ^ quote x) else ()
   1.876 @@ -700,60 +466,61 @@
   1.877  
   1.878  
   1.879  
   1.880 -(** read and certify entities **)    (*exception ERROR/TYPE*)
   1.881 +(** read and certify entities **)    (*exception ERROR*)
   1.882  
   1.883  (* sorts *)
   1.884  
   1.885 -fun read_sort' syn sg str =
   1.886 +fun read_sort' syn thy str =
   1.887    let
   1.888 -    val _ = check_stale "Sign.read_sort'" sg;
   1.889 -    val S = intern_sort sg (Syntax.read_sort syn str);
   1.890 -  in Type.cert_sort (tsig_of sg) S handle TYPE (msg, _, _) => error msg end;
   1.891 +    val _ = Context.check_thy "Sign.read_sort'" thy;
   1.892 +    val S = intern_sort thy (Syntax.read_sort syn str);
   1.893 +  in certify_sort thy S handle TYPE (msg, _, _) => error msg end;
   1.894  
   1.895 -fun read_sort sg str = read_sort' (syn_of sg) sg str;
   1.896 +fun read_sort thy str = read_sort' (syn_of thy) thy str;
   1.897  
   1.898  
   1.899  (* types *)
   1.900  
   1.901  local
   1.902  
   1.903 -fun gen_read_typ' cert syn (sg, def_sort) str =
   1.904 +fun gen_read_typ' cert syn (thy, def_sort) str =
   1.905    let
   1.906 -    val _ = check_stale "Sign.gen_read_typ'" sg;
   1.907 -    val get_sort = TypeInfer.get_sort (tsig_of sg) def_sort (intern_sort sg);
   1.908 -    val T = intern_tycons sg (Syntax.read_typ syn get_sort (intern_sort sg) str);
   1.909 -  in cert (tsig_of sg) T handle TYPE (msg, _, _) => error msg end
   1.910 +    val _ = Context.check_thy "Sign.gen_read_typ'" thy;
   1.911 +    val get_sort = TypeInfer.get_sort (tsig_of thy) def_sort (intern_sort thy);
   1.912 +    val T = intern_tycons thy (Syntax.read_typ syn get_sort (intern_sort thy) str);
   1.913 +  in cert thy T handle TYPE (msg, _, _) => error msg end
   1.914    handle ERROR => error ("The error(s) above occurred in type " ^ quote str);
   1.915  
   1.916 -fun gen_read_typ cert (sg, def_sort) str = gen_read_typ' cert (syn_of sg) (sg, def_sort) str;
   1.917 +fun gen_read_typ cert (thy, def_sort) str =
   1.918 +  gen_read_typ' cert (syn_of thy) (thy, def_sort) str;
   1.919  
   1.920  in
   1.921  
   1.922 -fun no_def_sort sg = (sg, K NONE);
   1.923 +fun no_def_sort thy = (thy: theory, K NONE);
   1.924  
   1.925 -val read_typ'        = gen_read_typ' Type.cert_typ;
   1.926 -val read_typ_syntax' = gen_read_typ' Type.cert_typ_syntax;
   1.927 -val read_typ_abbrev' = gen_read_typ' Type.cert_typ_abbrev;
   1.928 -val read_typ         = gen_read_typ Type.cert_typ;
   1.929 -val read_typ_syntax  = gen_read_typ Type.cert_typ_syntax;
   1.930 -val read_typ_abbrev  = gen_read_typ Type.cert_typ_abbrev;
   1.931 +val read_typ'        = gen_read_typ' certify_typ;
   1.932 +val read_typ_syntax' = gen_read_typ' certify_typ_syntax;
   1.933 +val read_typ_abbrev' = gen_read_typ' certify_typ_abbrev;
   1.934 +val read_typ         = gen_read_typ certify_typ;
   1.935 +val read_typ_syntax  = gen_read_typ certify_typ_syntax;
   1.936 +val read_typ_abbrev  = gen_read_typ certify_typ_abbrev;
   1.937  
   1.938  end;
   1.939  
   1.940  
   1.941  (* type and constant names *)
   1.942  
   1.943 -fun read_tyname sg raw_c =
   1.944 -  let val c = intern_type sg raw_c in
   1.945 -    (case Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of sg))), c) of
   1.946 +fun read_tyname thy raw_c =
   1.947 +  let val c = intern_type thy raw_c in
   1.948 +    (case Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of thy))), c) of
   1.949        SOME (Type.LogicalType n, _) => Type (c, replicate n dummyT)
   1.950      | _ => error ("Undeclared type constructor: " ^ quote c))
   1.951    end;
   1.952  
   1.953 -fun read_const sg raw_c =
   1.954 +fun read_const thy raw_c =
   1.955    let
   1.956 -    val c = intern_const sg raw_c;
   1.957 -    val _ = the_const_type sg c handle TYPE (msg, _, _) => error msg;
   1.958 +    val c = intern_const thy raw_c;
   1.959 +    val _ = the_const_type thy c handle TYPE (msg, _, _) => error msg;
   1.960    in Const (c, dummyT) end;
   1.961  
   1.962  
   1.963 @@ -770,17 +537,15 @@
   1.964    typs: expected types
   1.965  *)
   1.966  
   1.967 -fun infer_types_simult pp sg def_type def_sort used freeze args =
   1.968 +fun infer_types_simult pp thy def_type def_sort used freeze args =
   1.969    let
   1.970 -    val tsig = tsig_of sg;
   1.971 -
   1.972      val termss = foldr multiply [[]] (map fst args);
   1.973      val typs =
   1.974 -      map (fn (_, T) => certify_typ sg T handle TYPE (msg, _, _) => error msg) args;
   1.975 +      map (fn (_, T) => certify_typ thy T handle TYPE (msg, _, _) => error msg) args;
   1.976  
   1.977 -    fun infer ts = OK (TypeInfer.infer_types (Syntax.pp_show_brackets pp) tsig
   1.978 -        (const_type sg) def_type def_sort (intern_const sg) (intern_tycons sg)
   1.979 -        (intern_sort sg) used freeze typs ts)
   1.980 +    fun infer ts = OK (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
   1.981 +        (const_type thy) def_type def_sort (intern_const thy) (intern_tycons thy)
   1.982 +        (intern_sort thy) used freeze typs ts)
   1.983        handle TYPE (msg, _, _) => Error msg;
   1.984  
   1.985      val err_results = map infer termss;
   1.986 @@ -806,26 +571,25 @@
   1.987        cat_lines (map (Pretty.string_of_term pp) (List.concat (map fst results)))))
   1.988    end;
   1.989  
   1.990 -
   1.991 -fun infer_types pp sg def_type def_sort used freeze tsT =
   1.992 -  apfst hd (infer_types_simult pp sg def_type def_sort used freeze [tsT]);
   1.993 +fun infer_types pp thy def_type def_sort used freeze tsT =
   1.994 +  apfst hd (infer_types_simult pp thy def_type def_sort used freeze [tsT]);
   1.995  
   1.996  
   1.997  
   1.998 -(** read_def_terms -- read terms and infer types **)
   1.999 +(** read_def_terms -- read terms and infer types **)    (*exception ERROR*)
  1.1000  
  1.1001 -fun read_def_terms' pp is_logtype syn (sg, types, sorts) used freeze sTs =
  1.1002 +fun read_def_terms' pp is_logtype syn (thy, types, sorts) used freeze sTs =
  1.1003    let
  1.1004      fun read (s, T) =
  1.1005 -      let val T' = certify_typ sg T handle TYPE (msg, _, _) => error msg
  1.1006 +      let val T' = certify_typ thy T handle TYPE (msg, _, _) => error msg
  1.1007        in (Syntax.read is_logtype syn T' s, T') end;
  1.1008 -  in infer_types_simult pp sg types sorts used freeze (map read sTs) end;
  1.1009 +  in infer_types_simult pp thy types sorts used freeze (map read sTs) end;
  1.1010  
  1.1011 -fun read_def_terms (sg, types, sorts) =
  1.1012 -  read_def_terms' (pp sg) (is_logtype sg) (syn_of sg) (sg, types, sorts);
  1.1013 +fun read_def_terms (thy, types, sorts) =
  1.1014 +  read_def_terms' (pp thy) (is_logtype thy) (syn_of thy) (thy, types, sorts);
  1.1015  
  1.1016 -fun simple_read_term sg T s =
  1.1017 -  let val ([t], _) = read_def_terms (sg, K NONE, K NONE) [] true [(s, T)]
  1.1018 +fun simple_read_term thy T s =
  1.1019 +  let val ([t], _) = read_def_terms (thy, K NONE, K NONE) [] true [(s, T)]
  1.1020    in t end
  1.1021    handle ERROR => error ("The error(s) above occurred for term " ^ s);
  1.1022  
  1.1023 @@ -835,8 +599,8 @@
  1.1024  
  1.1025  (* add default sort *)
  1.1026  
  1.1027 -fun gen_add_defsort prep_sort s sg =
  1.1028 -  sg |> map_tsig (Type.set_defsort (prep_sort sg s));
  1.1029 +fun gen_add_defsort prep_sort s thy =
  1.1030 +  thy |> map_tsig (Type.set_defsort (prep_sort thy s));
  1.1031  
  1.1032  val add_defsort = gen_add_defsort read_sort;
  1.1033  val add_defsort_i = gen_add_defsort certify_sort;
  1.1034 @@ -844,34 +608,41 @@
  1.1035  
  1.1036  (* add type constructors *)
  1.1037  
  1.1038 -fun add_types types sg = sg |> map_sign (fn (syn, tsig, consts) =>
  1.1039 +fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
  1.1040    let
  1.1041      val syn' = map_syntax (Syntax.extend_type_gram types) syn;
  1.1042      val decls = map (fn (a, n, mx) => (Syntax.type_name a mx, n)) types;
  1.1043 -    val tsig' = Type.add_types (naming_of sg) decls tsig;
  1.1044 -  in (syn', tsig', consts) end);
  1.1045 +    val tsig' = Type.add_types naming decls tsig;
  1.1046 +  in (naming, syn', tsig', consts) end);
  1.1047 +
  1.1048 +fun add_typedecls decls thy =
  1.1049 +  let
  1.1050 +    fun type_of (a, vs, mx) =
  1.1051 +      if null (duplicates vs) then (a, length vs, mx)
  1.1052 +      else error ("Duplicate parameters in type declaration: " ^ quote a);
  1.1053 +  in add_types (map type_of decls) thy end;
  1.1054  
  1.1055  
  1.1056  (* add nonterminals *)
  1.1057  
  1.1058 -fun add_nonterminals bnames sg = sg |> map_sign (fn (syn, tsig, consts) =>
  1.1059 +fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
  1.1060    let
  1.1061 -    val syn' = map_syntax (Syntax.extend_consts bnames) syn;
  1.1062 -    val tsig' = Type.add_nonterminals (naming_of sg) bnames tsig;
  1.1063 -  in (syn', tsig', consts) end);
  1.1064 +    val syn' = map_syntax (Syntax.extend_consts ns) syn;
  1.1065 +    val tsig' = Type.add_nonterminals naming ns tsig;
  1.1066 +  in (naming, syn', tsig', consts) end);
  1.1067  
  1.1068  
  1.1069  (* add type abbreviations *)
  1.1070  
  1.1071 -fun gen_add_tyabbr prep_typ (a, vs, rhs, mx) sg =
  1.1072 -  sg |> map_sign (fn (syn, tsig, consts) =>
  1.1073 +fun gen_add_tyabbr prep_typ (a, vs, rhs, mx) thy =
  1.1074 +  thy |> map_sign (fn (naming, syn, tsig, consts) =>
  1.1075      let
  1.1076        val syn' = map_syntax (Syntax.extend_type_gram [(a, length vs, mx)]) syn;
  1.1077        val a' = Syntax.type_name a mx;
  1.1078 -      val abbr = (a', vs, prep_typ sg rhs) handle ERROR =>
  1.1079 -        error ("in type abbreviation " ^ quote a');
  1.1080 -      val tsig' = Type.add_abbrevs (naming_of sg) [abbr] tsig;
  1.1081 -    in (syn', tsig', consts) end);
  1.1082 +      val abbr = (a', vs, prep_typ thy rhs)
  1.1083 +        handle ERROR => error ("in type abbreviation " ^ quote a');
  1.1084 +      val tsig' = Type.add_abbrevs naming [abbr] tsig;
  1.1085 +    in (naming, syn', tsig', consts) end);
  1.1086  
  1.1087  val add_tyabbrs = fold (gen_add_tyabbr (read_typ_syntax o no_def_sort));
  1.1088  val add_tyabbrs_i = fold (gen_add_tyabbr certify_typ_syntax);
  1.1089 @@ -879,11 +650,11 @@
  1.1090  
  1.1091  (* add type arities *)
  1.1092  
  1.1093 -fun gen_add_arities int_type prep_sort arities sg = sg |> map_tsig (fn tsig =>
  1.1094 +fun gen_add_arities int_type prep_sort arities thy = thy |> map_tsig (fn tsig =>
  1.1095    let
  1.1096 -    fun prep_arity (a, Ss, S) = (int_type sg a, map (prep_sort sg) Ss, prep_sort sg S)
  1.1097 +    fun prep_arity (a, Ss, S) = (int_type thy a, map (prep_sort thy) Ss, prep_sort thy S)
  1.1098        handle ERROR => error ("in arity for type " ^ quote a);
  1.1099 -    val tsig' = Type.add_arities (pp sg) (map prep_arity arities) tsig;
  1.1100 +    val tsig' = Type.add_arities (pp thy) (map prep_arity arities) tsig;
  1.1101    in tsig' end);
  1.1102  
  1.1103  val add_arities = gen_add_arities intern_type read_sort;
  1.1104 @@ -892,37 +663,39 @@
  1.1105  
  1.1106  (* modify syntax *)
  1.1107  
  1.1108 -fun gen_syntax change_gram prep_typ (prmode, args) sg =
  1.1109 +fun gen_syntax change_gram prep_typ prmode args thy =
  1.1110    let
  1.1111 -    fun prep (c, T, mx) = (c, prep_typ sg T, mx) handle ERROR =>
  1.1112 -      error ("in syntax declaration " ^ quote (Syntax.const_name c mx));
  1.1113 -  in sg |> map_syn (map_syntax (change_gram (is_logtype sg) prmode (map prep args))) end;
  1.1114 +    fun prep (c, T, mx) = (c, prep_typ thy T, mx)
  1.1115 +      handle ERROR => error ("in syntax declaration " ^ quote (Syntax.const_name c mx));
  1.1116 +  in thy |> map_syn (map_syntax (change_gram (is_logtype thy) prmode (map prep args))) end;
  1.1117  
  1.1118  fun gen_add_syntax x = gen_syntax Syntax.extend_const_gram x;
  1.1119  
  1.1120  val add_modesyntax = gen_add_syntax (read_typ_syntax o no_def_sort);
  1.1121  val add_modesyntax_i = gen_add_syntax certify_typ_syntax;
  1.1122 -val add_syntax = curry add_modesyntax Syntax.default_mode;
  1.1123 -val add_syntax_i = curry add_modesyntax_i Syntax.default_mode;
  1.1124 +val add_syntax = add_modesyntax Syntax.default_mode;
  1.1125 +val add_syntax_i = add_modesyntax_i Syntax.default_mode;
  1.1126  val del_modesyntax = gen_syntax Syntax.remove_const_gram (read_typ_syntax o no_def_sort);
  1.1127  val del_modesyntax_i = gen_syntax Syntax.remove_const_gram certify_typ_syntax;
  1.1128  
  1.1129  
  1.1130  (* add constants *)
  1.1131  
  1.1132 -fun err_dup_consts cs =
  1.1133 -  error ("Duplicate declaration of constant(s) " ^ commas_quote cs);
  1.1134 -
  1.1135 -fun gen_add_consts prep_typ raw_args sg =
  1.1136 +fun gen_add_consts prep_typ raw_args thy =
  1.1137    let
  1.1138 -    val prepT = compress_type o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ sg;
  1.1139 +    val prepT = compress_type o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
  1.1140      fun prep (c, T, mx) = ((c, prepT T, mx) handle TYPE (msg, _, _) => error msg)
  1.1141        handle ERROR => error ("in declaration of constant " ^ quote (Syntax.const_name c mx));
  1.1142      val args = map prep raw_args;
  1.1143      val decls = args |> map (fn (c, T, mx) => (Syntax.const_name c mx, (T, stamp ())));
  1.1144 -    fun extend_consts consts = NameSpace.extend_table (naming_of sg) (consts, decls)
  1.1145 +
  1.1146 +    fun extend_consts consts = NameSpace.extend_table (naming_of thy) (consts, decls)
  1.1147        handle Symtab.DUPS cs => err_dup_consts cs;
  1.1148 -  in sg |> map_consts extend_consts |> add_syntax_i args end;
  1.1149 +  in
  1.1150 +    thy
  1.1151 +    |> map_consts extend_consts
  1.1152 +    |> add_syntax_i args
  1.1153 +  end;
  1.1154  
  1.1155  val add_consts = gen_add_consts (read_typ o no_def_sort);
  1.1156  val add_consts_i = gen_add_consts certify_typ;
  1.1157 @@ -936,13 +709,13 @@
  1.1158  fun class_of_const c = unsuffix classN c
  1.1159    handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
  1.1160  
  1.1161 -fun gen_add_class int_class (bclass, raw_classes) sg =
  1.1162 -  sg |> map_sign (fn (syn, tsig, consts) =>
  1.1163 +fun gen_add_class int_class (bclass, raw_classes) thy =
  1.1164 +  thy |> map_sign (fn (naming, syn, tsig, consts) =>
  1.1165      let
  1.1166 -      val classes = map (int_class sg) raw_classes;
  1.1167 +      val classes = map (int_class thy) raw_classes;
  1.1168        val syn' = map_syntax (Syntax.extend_consts [bclass]) syn;
  1.1169 -      val tsig' = Type.add_classes (pp sg) (naming_of sg) [(bclass, classes)] tsig;
  1.1170 -    in (syn', tsig', consts) end)
  1.1171 +      val tsig' = Type.add_classes (pp thy) naming [(bclass, classes)] tsig;
  1.1172 +    in (naming, syn', tsig', consts) end)
  1.1173    |> add_consts_i [(const_of_class bclass, a_itselfT --> propT, Syntax.NoSyn)];
  1.1174  
  1.1175  val add_classes = fold (gen_add_class intern_class);
  1.1176 @@ -951,10 +724,10 @@
  1.1177  
  1.1178  (* add to classrel *)
  1.1179  
  1.1180 -fun gen_add_classrel int_class raw_pairs sg = sg |> map_tsig (fn tsig =>
  1.1181 +fun gen_add_classrel int_class raw_pairs thy = thy |> map_tsig (fn tsig =>
  1.1182    let
  1.1183 -    val pairs = map (pairself (int_class sg)) raw_pairs;
  1.1184 -    val tsig' = Type.add_classrel (pp sg) pairs tsig;
  1.1185 +    val pairs = map (pairself (int_class thy)) raw_pairs;
  1.1186 +    val tsig' = Type.add_classrel (pp thy) pairs tsig;
  1.1187    in tsig' end);
  1.1188  
  1.1189  val add_classrel = gen_add_classrel intern_class;
  1.1190 @@ -967,13 +740,13 @@
  1.1191  
  1.1192  fun mk trs = map Syntax.mk_trfun trs;
  1.1193  
  1.1194 -fun gen_add_trfuns ext non_typed (atrs, trs, tr's, atr's) sg = sg |> map_syn (fn syn =>
  1.1195 +fun gen_add_trfuns ext non_typed (atrs, trs, tr's, atr's) thy = thy |> map_syn (fn syn =>
  1.1196    let val syn' = syn |> ext (mk atrs, mk trs, mk (map (apsnd non_typed) tr's), mk atr's)
  1.1197 -  in make_syntax sg syn'; syn' end);
  1.1198 +  in make_syntax thy syn'; syn' end);
  1.1199  
  1.1200 -fun gen_add_trfunsT ext tr's sg = sg |> map_syn (fn syn =>
  1.1201 +fun gen_add_trfunsT ext tr's thy = thy |> map_syn (fn syn =>
  1.1202    let val syn' = syn |> ext ([], [], mk tr's, [])
  1.1203 -  in make_syntax sg syn'; syn' end);
  1.1204 +  in make_syntax thy syn'; syn' end);
  1.1205  
  1.1206  in
  1.1207  
  1.1208 @@ -985,13 +758,14 @@
  1.1209  end;
  1.1210  
  1.1211  val add_tokentrfuns = map_syn o map_syntax o Syntax.extend_tokentrfuns;
  1.1212 +fun add_mode_tokentrfuns m = add_tokentrfuns o map (fn (s, f) => (m, s, f));
  1.1213  
  1.1214  
  1.1215  (* add translation rules *)
  1.1216  
  1.1217 -fun add_trrules args sg = sg |> map_syn (fn syn =>
  1.1218 -  let val rules = map (Syntax.map_trrule (apfst (intern_type sg))) args
  1.1219 -  in map_syntax (Syntax.extend_trrules (is_logtype sg) (make_syntax sg syn) rules) syn end);
  1.1220 +fun add_trrules args thy = thy |> map_syn (fn syn =>
  1.1221 +  let val rules = map (Syntax.map_trrule (apfst (intern_type thy))) args
  1.1222 +  in map_syntax (Syntax.extend_trrules (is_logtype thy) (make_syntax thy syn) rules) syn end);
  1.1223  
  1.1224  val add_trrules_i = map_syn o map_syntax o Syntax.extend_trrules_i;
  1.1225  
  1.1226 @@ -1005,89 +779,21 @@
  1.1227  val set_policy      = map_naming o NameSpace.set_policy;
  1.1228  val restore_naming  = map_naming o K o naming_of;
  1.1229  
  1.1230 +val parent_path     = add_path "..";
  1.1231 +val root_path       = add_path "/";
  1.1232 +val absolute_path   = add_path "//";
  1.1233 +
  1.1234 +fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
  1.1235 +
  1.1236  
  1.1237  (* hide names *)
  1.1238  
  1.1239 -fun hide_classes b xs sg = sg |> map_tsig (Type.hide_classes b (map (intern_class sg) xs));
  1.1240 +fun hide_classes b xs thy = thy |> map_tsig (Type.hide_classes b (map (intern_class thy) xs));
  1.1241  val hide_classes_i = map_tsig oo Type.hide_classes;
  1.1242 -fun hide_types b xs sg = sg |> map_tsig (Type.hide_types b (map (intern_type sg) xs));
  1.1243 +fun hide_types b xs thy = thy |> map_tsig (Type.hide_types b (map (intern_type thy) xs));
  1.1244  val hide_types_i = map_tsig oo Type.hide_types;
  1.1245 -fun hide_consts b xs sg =
  1.1246 -  sg |> map_consts (apfst (fold (NameSpace.hide b o intern_const sg) xs));
  1.1247 +fun hide_consts b xs thy =
  1.1248 +  thy |> map_consts (apfst (fold (NameSpace.hide b o intern_const thy) xs));
  1.1249  val hide_consts_i = (map_consts o apfst) oo (fold o NameSpace.hide);
  1.1250  
  1.1251 -
  1.1252 -
  1.1253 -(** merge signatures **)
  1.1254 -
  1.1255 -fun merge_stamps stamps1 stamps2 =
  1.1256 -  let val stamps = merge_lists' stamps1 stamps2 in
  1.1257 -    (case duplicates (map ! stamps) of
  1.1258 -      [] => stamps
  1.1259 -    | dups => error ("Attempt to merge different versions of theories " ^ commas_quote dups))
  1.1260 -  end;
  1.1261 -
  1.1262 -
  1.1263 -(* trivial merge *)
  1.1264 -
  1.1265 -fun merge_refs (sgr1 as SgRef (SOME (ref (sg1 as Sg ({stamps = s1, ...}, _)))),
  1.1266 -        sgr2 as SgRef (SOME (ref (sg2 as Sg ({stamps = s2, ...}, _))))) =
  1.1267 -      if subsig (sg2, sg1) then sgr1
  1.1268 -      else if subsig (sg1, sg2) then sgr2
  1.1269 -      else (merge_stamps s1 s2;  (*check for different versions*)
  1.1270 -        error ("Attempt to do non-trivial merge of signature\n" ^
  1.1271 -          str_of_sg sg1 ^ " and " ^ str_of_sg sg2))
  1.1272 -  | merge_refs _ = sys_error "Sign.merge_refs";
  1.1273 -
  1.1274 -val merge = deref o merge_refs o pairself self_ref;
  1.1275 -
  1.1276 -
  1.1277 -(* non-trivial merge *)              (*exception TERM/ERROR*)
  1.1278 -
  1.1279 -local
  1.1280 -
  1.1281 -fun nontriv_merge (sg1, sg2) =
  1.1282 -  if subsig_internal (sg2, sg1) then sg1
  1.1283 -  else if subsig_internal (sg1, sg2) then sg2
  1.1284 -  else
  1.1285 -    if exists_stamp CPureN sg1 <> exists_stamp CPureN sg2
  1.1286 -    then error "Cannot merge Pure and CPure developments"
  1.1287 -  else
  1.1288 -    let
  1.1289 -      val Sg ({id = _, stamps = stamps1, syn = Syn (syntax1, trfuns1)},
  1.1290 -          {self = _, tsig = tsig1, consts = consts1, naming = _, data = data1}) = sg1;
  1.1291 -      val Sg ({id = _, stamps = stamps2, syn = Syn (syntax2, trfuns2)},
  1.1292 -          {self = _, tsig = tsig2, consts = consts2, naming = _, data = data2}) = sg2;
  1.1293 -
  1.1294 -      val stamps = merge_stamps stamps1 stamps2;
  1.1295 -      val syntax = Syntax.merge_syntaxes syntax1 syntax2;
  1.1296 -      val trfuns = merge_trfuns trfuns1 trfuns2;
  1.1297 -      val syn = Syn (syntax, trfuns);
  1.1298 -      val consts = NameSpace.merge_tables eq_snd (consts1, consts2)
  1.1299 -        handle Symtab.DUPS cs => err_dup_consts cs;
  1.1300 -      val naming = NameSpace.default_naming;
  1.1301 -      val data = merge_data (data1, data2);
  1.1302 -
  1.1303 -      val pre_sg = make_sg (ref "", SgRef (SOME (ref dummy_sg)), ref "#" :: stamps1)
  1.1304 -        naming data (syn, tsig1, consts);
  1.1305 -      val tsig = Type.merge_tsigs (pp pre_sg) (tsig1, tsig2);
  1.1306 -
  1.1307 -      val self = SgRef (SOME (ref dummy_sg));
  1.1308 -      val sg = make_sg (ref "", self, stamps) naming data (syn, tsig, consts);
  1.1309 -    in assign self sg; syn_of sg; sg end;
  1.1310 -
  1.1311 -in
  1.1312 -
  1.1313 -fun prep_ext_merge sgs =
  1.1314 -  if null sgs then
  1.1315 -    error "Merge: no parent theories"
  1.1316 -  else if exists is_draft sgs then
  1.1317 -    error "Attempt to merge draft theories"
  1.1318 -  else
  1.1319 -    Library.foldl nontriv_merge (hd sgs, tl sgs)
  1.1320 -    |> prep_ext
  1.1321 -    |> add_path "/";
  1.1322 -
  1.1323  end;
  1.1324 -
  1.1325 -end;