# 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) ();