# HG changeset patch
# User wenzelm
# Date 925817573 -7200
# Node ID a91b4cfd3104d8a9e989303c90b16797f0c27a87
# Parent  0fc9763762be82c67f0d8848351a888296c9ec6a
transaction: Theory.copy;

diff -r 0fc9763762be -r a91b4cfd3104 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue May 04 13:32:35 1999 +0200
+++ b/src/Pure/pure_thy.ML	Tue May 04 13:32:53 1999 +0200
@@ -372,7 +372,7 @@
     val {name, generation} = get_info thy;
     val copy_thy =
       thy
-      |> Theory.prep_ext
+      |> Theory.copy
       |> Theory.add_name ("#" ^ name ^ ":" ^ string_of_int generation)  (* FIXME !!?? *)
       |> put_info {name = name, generation = generation + 1};
     val (thy', opt_exn) = (transform_error f thy, None) handle exn => (thy, Some exn);