# HG changeset patch
# User wenzelm
# Date 911046316 -3600
# Node ID 3a1f9ec7c8a29c2d1eaedd12274dc688440560ac
# Parent  7536314d9a5fc251c21c3a977695b20371368f9c
val copy: theory -> theory;

diff -r 7536314d9a5f -r 3a1f9ec7c8a2 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sat Nov 14 13:24:20 1998 +0100
+++ b/src/Pure/theory.ML	Sat Nov 14 13:25:16 1998 +0100
@@ -78,6 +78,7 @@
   val root_path: theory -> theory
   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 requires: theory -> string -> string -> unit
@@ -206,7 +207,7 @@
 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             = prep_ext;	(*an approximation ...*)
 
 
 (** add axioms **)