hide prep_ext, merge_theories;
authorwenzelm
Tue, 04 May 1999 13:32:35 +0200
changeset 6573 0fc9763762be
parent 6572 e77641d2f4ac
child 6574 a91b4cfd3104
hide prep_ext, merge_theories;
src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue May 04 11:31:29 1999 +0200
+++ b/src/Pure/theory.ML	Tue May 04 13:32:35 1999 +0200
@@ -28,7 +28,6 @@
     string list -> string * string -> string * term
   val read_axm: Sign.sg -> string * string -> string * term
   val inferT_axm: Sign.sg -> string * term -> string * term
-  val merge_theories: string -> theory * theory -> theory
 end
 
 signature THEORY =
@@ -81,8 +80,8 @@
   val add_space: string * string list -> theory -> theory
   val add_name: string -> theory -> theory
   val copy: theory -> theory
-  val prep_ext: theory -> theory
   val prep_ext_merge: theory list -> theory
+  val merge_theories: string -> theory * theory -> theory
   val requires: theory -> string -> string -> unit
   val assert_super: theory -> theory -> theory
   val pre_pure: theory
@@ -211,7 +210,6 @@
 val root_path        = add_path "/";
 val add_space        = ext_sign Sign.add_space;
 val add_name         = ext_sign Sign.add_name;
-val prep_ext         = ext_sign (K Sign.prep_ext) ();
 val copy             = ext_sign (K Sign.copy) ();