# HG changeset patch
# User wenzelm
# Date 877336744 -7200
# Node ID 5ccabd20574c160e111907e0cfcf9380732fe1a3
# Parent  436463f9f2b4f95fa7e0329c7b1ecb0330efaa3d
fixed types of add_XXX;

diff -r 436463f9f2b4 -r 5ccabd20574c src/Pure/theory.ML
--- 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