tuned types;
authorwenzelm
Mon Oct 20 15:20:20 1997 +0200 (1997-10-20)
changeset 3956d59fe4579004
parent 3955 9666a1ecf3a1
child 3957 7914990748ad
tuned types;
src/Pure/axclass.ML
src/Pure/sign.ML
src/Pure/theory.ML
     1.1 --- a/src/Pure/axclass.ML	Mon Oct 20 15:18:09 1997 +0200
     1.2 +++ b/src/Pure/axclass.ML	Mon Oct 20 15:20:20 1997 +0200
     1.3 @@ -10,9 +10,9 @@
     1.4    val add_thms_as_axms: (string * thm) list -> theory -> theory
     1.5    val add_classrel_thms: thm list -> theory -> theory
     1.6    val add_arity_thms: thm list -> theory -> theory
     1.7 -  val add_axclass: rclass * xclass list -> (string * string) list
     1.8 +  val add_axclass: bclass * xclass list -> (string * string) list
     1.9      -> theory -> theory
    1.10 -  val add_axclass_i: rclass * class list -> (string * term) list
    1.11 +  val add_axclass_i: bclass * class list -> (string * term) list
    1.12      -> theory -> theory
    1.13    val add_inst_subclass: xclass * xclass -> string list -> thm list
    1.14      -> tactic option -> theory -> theory
     2.1 --- a/src/Pure/sign.ML	Mon Oct 20 15:18:09 1997 +0200
     2.2 +++ b/src/Pure/sign.ML	Mon Oct 20 15:20:20 1997 +0200
     2.3 @@ -5,10 +5,10 @@
     2.4  The abstract type "sg" of signatures.
     2.5  *)
     2.6  
     2.7 -(*raw base names*)
     2.8 -type rstring = string;
     2.9 -type rclass = class;
    2.10 -(*external pruned forms*)
    2.11 +(*base names*)
    2.12 +type bstring = string;
    2.13 +type bclass = class;
    2.14 +(*external forms -- partially qualified names*)
    2.15  type xstring = string;
    2.16  type xclass = class;
    2.17  type xsort = sort;
    2.18 @@ -40,8 +40,8 @@
    2.19    val classK: string
    2.20    val typeK: string
    2.21    val constK: string
    2.22 -  val full_name: sg -> rstring -> string
    2.23 -  val base_name: string -> rstring
    2.24 +  val full_name: sg -> bstring -> string
    2.25 +  val base_name: string -> bstring
    2.26    val intern: sg -> string -> xstring -> string
    2.27    val extern: sg -> string -> string -> xstring
    2.28    val cond_extern: sg -> string -> string -> xstring
    2.29 @@ -72,30 +72,30 @@
    2.30    val infer_types: sg -> (indexname -> typ option) ->
    2.31      (indexname -> sort option) -> string list -> bool
    2.32      -> xterm list * typ -> int * term * (indexname * typ) list
    2.33 -  val add_classes: (rclass * xclass list) list -> sg -> sg
    2.34 -  val add_classes_i: (rclass * class list) list -> sg -> sg
    2.35 +  val add_classes: (bclass * xclass list) list -> sg -> sg
    2.36 +  val add_classes_i: (bclass * class list) list -> sg -> sg
    2.37    val add_classrel: (xclass * xclass) list -> sg -> sg
    2.38    val add_classrel_i: (class * class) list -> sg -> sg
    2.39    val add_defsort: xsort -> sg -> sg
    2.40    val add_defsort_i: sort -> sg -> sg
    2.41 -  val add_types: (rstring * int * mixfix) list -> sg -> sg
    2.42 -  val add_tyabbrs: (rstring * string list * string * mixfix) list -> sg -> sg
    2.43 -  val add_tyabbrs_i: (rstring * string list * typ * mixfix) list -> sg -> sg
    2.44 +  val add_types: (bstring * int * mixfix) list -> sg -> sg
    2.45 +  val add_tyabbrs: (bstring * string list * string * mixfix) list -> sg -> sg
    2.46 +  val add_tyabbrs_i: (bstring * string list * typ * mixfix) list -> sg -> sg
    2.47    val add_arities: (xstring * xsort list * xsort) list -> sg -> sg
    2.48    val add_arities_i: (string * sort list * sort) list -> sg -> sg
    2.49 -  val add_consts: (rstring * string * mixfix) list -> sg -> sg
    2.50 -  val add_consts_i: (rstring * typ * mixfix) list -> sg -> sg
    2.51 -  val add_syntax: (rstring * string * mixfix) list -> sg -> sg
    2.52 -  val add_syntax_i: (rstring * typ * mixfix) list -> sg -> sg
    2.53 -  val add_modesyntax: (string * bool) * (rstring * string * mixfix) list -> sg -> sg
    2.54 -  val add_modesyntax_i: (string * bool) * (rstring * typ * mixfix) list -> sg -> sg
    2.55 +  val add_consts: (bstring * string * mixfix) list -> sg -> sg
    2.56 +  val add_consts_i: (bstring * typ * mixfix) list -> sg -> sg
    2.57 +  val add_syntax: (bstring * string * mixfix) list -> sg -> sg
    2.58 +  val add_syntax_i: (bstring * typ * mixfix) list -> sg -> sg
    2.59 +  val add_modesyntax: (string * bool) * (bstring * string * mixfix) list -> sg -> sg
    2.60 +  val add_modesyntax_i: (string * bool) * (bstring * typ * mixfix) list -> sg -> sg
    2.61    val add_trfuns:
    2.62 -    (string * (ast list -> ast)) list *
    2.63 -    (string * (term list -> term)) list *
    2.64 -    (string * (term list -> term)) list *
    2.65 -    (string * (ast list -> ast)) list -> sg -> sg
    2.66 +    (bstring * (ast list -> ast)) list *
    2.67 +    (bstring * (term list -> term)) list *
    2.68 +    (bstring * (term list -> term)) list *
    2.69 +    (bstring * (ast list -> ast)) list -> sg -> sg
    2.70    val add_trfunsT:
    2.71 -    (string * (typ -> term list -> term)) list -> sg -> sg
    2.72 +    (bstring * (typ -> term list -> term)) list -> sg -> sg
    2.73    val add_tokentrfuns:
    2.74      (string * string * (string -> string * int)) list -> sg -> sg
    2.75    val add_trrules: (string * string) Syntax.trrule list -> sg -> sg
     3.1 --- a/src/Pure/theory.ML	Mon Oct 20 15:18:09 1997 +0200
     3.2 +++ b/src/Pure/theory.ML	Mon Oct 20 15:20:20 1997 +0200
     3.3 @@ -37,41 +37,41 @@
     3.4    val thmK		: string
     3.5    val oracleK		: string
     3.6    (*theory extendsion primitives*)
     3.7 -  val add_classes	: (rclass * xclass list) list -> theory -> theory
     3.8 -  val add_classes_i	: (rclass * class list) list -> theory -> theory
     3.9 +  val add_classes	: (bclass * xclass list) list -> theory -> theory
    3.10 +  val add_classes_i	: (bclass * class list) list -> theory -> theory
    3.11    val add_classrel	: (xclass * xclass) list -> theory -> theory
    3.12    val add_classrel_i	: (class * class) list -> theory -> theory
    3.13    val add_defsort	: xsort -> theory -> theory
    3.14    val add_defsort_i	: sort -> theory -> theory
    3.15 -  val add_types		: (rstring * int * mixfix) list -> theory -> theory
    3.16 -  val add_tyabbrs	: (rstring * string list * string * mixfix) list
    3.17 +  val add_types		: (bstring * int * mixfix) list -> theory -> theory
    3.18 +  val add_tyabbrs	: (bstring * string list * string * mixfix) list
    3.19      -> theory -> theory
    3.20 -  val add_tyabbrs_i	: (rstring * string list * typ * mixfix) list
    3.21 +  val add_tyabbrs_i	: (bstring * string list * typ * mixfix) list
    3.22      -> theory -> theory
    3.23    val add_arities	: (xstring * xsort list * xsort) list -> theory -> theory
    3.24    val add_arities_i	: (string * sort list * sort) list -> theory -> theory
    3.25 -  val add_consts	: (rstring * string * mixfix) list -> theory -> theory
    3.26 -  val add_consts_i	: (rstring * typ * mixfix) list -> theory -> theory
    3.27 -  val add_syntax	: (rstring * string * mixfix) list -> theory -> theory
    3.28 -  val add_syntax_i	: (rstring * typ * mixfix) list -> theory -> theory
    3.29 -  val add_modesyntax	: string * bool -> (rstring * string * mixfix) list -> theory -> theory
    3.30 -  val add_modesyntax_i	: string * bool -> (rstring * typ * mixfix) list -> theory -> theory
    3.31 +  val add_consts	: (bstring * string * mixfix) list -> theory -> theory
    3.32 +  val add_consts_i	: (bstring * typ * mixfix) list -> theory -> theory
    3.33 +  val add_syntax	: (bstring * string * mixfix) list -> theory -> theory
    3.34 +  val add_syntax_i	: (bstring * typ * mixfix) list -> theory -> theory
    3.35 +  val add_modesyntax	: string * bool -> (bstring * string * mixfix) list -> theory -> theory
    3.36 +  val add_modesyntax_i	: string * bool -> (bstring * typ * mixfix) list -> theory -> theory
    3.37    val add_trfuns	:
    3.38 -    (string * (Syntax.ast list -> Syntax.ast)) list *
    3.39 -    (string * (term list -> term)) list *
    3.40 -    (string * (term list -> term)) list *
    3.41 -    (string * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory
    3.42 +    (bstring * (Syntax.ast list -> Syntax.ast)) list *
    3.43 +    (bstring * (term list -> term)) list *
    3.44 +    (bstring * (term list -> term)) list *
    3.45 +    (bstring * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory
    3.46    val add_trfunsT	:
    3.47 -    (string * (typ -> term list -> term)) list -> theory -> theory
    3.48 +    (bstring * (typ -> term list -> term)) list -> theory -> theory
    3.49    val add_tokentrfuns:
    3.50      (string * string * (string -> string * int)) list -> theory -> theory
    3.51    val add_trrules	: (string * string) Syntax.trrule list -> theory -> theory
    3.52    val add_trrules_i	: Syntax.ast Syntax.trrule list -> theory -> theory
    3.53 -  val add_axioms	: (rstring * string) list -> theory -> theory
    3.54 -  val add_axioms_i	: (rstring * term) list -> theory -> theory
    3.55 -  val add_oracle	: rstring * (Sign.sg * exn -> term) -> theory -> theory
    3.56 -  val add_defs		: (rstring * string) list -> theory -> theory
    3.57 -  val add_defs_i	: (rstring * term) list -> theory -> theory
    3.58 +  val add_axioms	: (bstring * string) list -> theory -> theory
    3.59 +  val add_axioms_i	: (bstring * term) list -> theory -> theory
    3.60 +  val add_oracle	: bstring * (Sign.sg * exn -> term) -> theory -> theory
    3.61 +  val add_defs		: (bstring * string) list -> theory -> theory
    3.62 +  val add_defs_i	: (bstring * term) list -> theory -> theory
    3.63    val add_path		: string -> theory -> theory
    3.64    val add_space		: string * string list -> theory -> theory
    3.65    val add_name		: string -> theory -> theory