src/Pure/theory.ML

--- a/src/Pure/theory.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/Pure/theory.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -86,7 +86,6 @@
   val hide_consts: string list -> theory -> theory
   val add_name: string -> theory -> theory
   val copy: theory -> theory
-  val finish: theory -> theory
   val prep_ext: theory -> theory
   val prep_ext_merge: theory list -> theory
   val requires: theory -> string -> string -> unit
@@ -98,8 +97,7 @@
 sig
   include THEORY
   val init_data: Object.kind -> (Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) *
-    (Object.T -> Object.T) * (Object.T * Object.T -> Object.T) *
-    (Sign.sg -> Object.T -> unit)) -> theory -> theory
+    (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit)) -> theory -> theory
   val print_data: Object.kind -> theory -> unit
   val get_data: Object.kind -> (Object.T -> 'a) -> theory -> 'a
   val put_data: Object.kind -> ('a -> Object.T) -> 'a -> theory -> theory
@@ -229,7 +227,6 @@
 val hide_consts      = curry hide_space_i Sign.constK;
 val add_name         = ext_sign Sign.add_name;
 val copy             = ext_sign (K Sign.copy) ();
-val finish           = ext_sign (K Sign.finish) ();
 val prep_ext         = ext_sign (K Sign.prep_ext) ();