--- a/src/Pure/theory.ML Mon Oct 20 10:38:36 1997 +0200
+++ b/src/Pure/theory.ML Mon Oct 20 10:39:04 1997 +0200
@@ -37,25 +37,25 @@
val thmK : string
val oracleK : string
(*theory extendsion primitives*)
- val add_classes : (xclass * xclass list) list -> theory -> theory
- val add_classes_i : (xclass * class list) list -> theory -> theory
+ val add_classes : (rclass * xclass list) list -> theory -> theory
+ val add_classes_i : (rclass * class list) list -> theory -> theory
val add_classrel : (xclass * xclass) list -> theory -> theory
val add_classrel_i : (class * class) list -> theory -> theory
val add_defsort : xsort -> theory -> theory
val add_defsort_i : sort -> theory -> theory
- val add_types : (xstring * int * mixfix) list -> theory -> theory
- val add_tyabbrs : (xstring * string list * string * mixfix) list
+ val add_types : (rstring * int * mixfix) list -> theory -> theory
+ val add_tyabbrs : (rstring * string list * string * mixfix) list
-> theory -> theory
- val add_tyabbrs_i : (xstring * string list * typ * mixfix) list
+ val add_tyabbrs_i : (rstring * string list * typ * mixfix) list
-> theory -> theory
val add_arities : (xstring * xsort list * xsort) list -> theory -> theory
val add_arities_i : (string * sort list * sort) list -> theory -> theory
- val add_consts : (xstring * string * mixfix) list -> theory -> theory
- val add_consts_i : (xstring * typ * mixfix) list -> theory -> theory
- val add_syntax : (xstring * string * mixfix) list -> theory -> theory
- val add_syntax_i : (xstring * typ * mixfix) list -> theory -> theory
- val add_modesyntax : string * bool -> (xstring * string * mixfix) list -> theory -> theory
- val add_modesyntax_i : string * bool -> (xstring * typ * mixfix) list -> theory -> theory
+ val add_consts : (rstring * string * mixfix) list -> theory -> theory
+ val add_consts_i : (rstring * typ * mixfix) list -> theory -> theory
+ val add_syntax : (rstring * string * mixfix) list -> theory -> theory
+ val add_syntax_i : (rstring * typ * mixfix) list -> theory -> theory
+ val add_modesyntax : string * bool -> (rstring * string * mixfix) list -> theory -> theory
+ val add_modesyntax_i : string * bool -> (rstring * typ * mixfix) list -> theory -> theory
val add_trfuns :
(string * (Syntax.ast list -> Syntax.ast)) list *
(string * (term list -> term)) list *
@@ -65,13 +65,13 @@
(string * (typ -> term list -> term)) list -> theory -> theory
val add_tokentrfuns:
(string * string * (string -> string * int)) list -> theory -> theory
- val add_trrules : (string * string)Syntax.trrule list -> theory -> theory
+ val add_trrules : (string * string) Syntax.trrule list -> theory -> theory
val add_trrules_i : Syntax.ast Syntax.trrule list -> theory -> theory
- val add_axioms : (xstring * string) list -> theory -> theory
- val add_axioms_i : (xstring * term) list -> theory -> theory
- val add_oracle : string * (Sign.sg * exn -> term) -> theory -> theory
- val add_defs : (xstring * string) list -> theory -> theory
- val add_defs_i : (xstring * term) list -> theory -> theory
+ val add_axioms : (rstring * string) list -> theory -> theory
+ val add_axioms_i : (rstring * term) list -> theory -> theory
+ val add_oracle : rstring * (Sign.sg * exn -> term) -> theory -> theory
+ val add_defs : (rstring * string) list -> theory -> theory
+ val add_defs_i : (rstring * term) list -> theory -> theory
val add_path : string -> theory -> theory
val add_space : string * string list -> theory -> theory
val add_name : string -> theory -> theory