# HG changeset patch
# User wenzelm
# Date 925817555 -7200
# Node ID 0fc9763762be82c67f0d8848351a888296c9ec6a
# Parent  e77641d2f4acb624efd6a1864943a72b46b9bdc6
hide prep_ext, merge_theories;

diff -r e77641d2f4ac -r 0fc9763762be 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) ();