# HG changeset patch
# User wenzelm
# Date 931112368 -7200
# Node ID 450b1f67f09954809266bb205d230a9dafe8cbd5
# Parent  b92c2f0413b851f5f7a8e80264abe218db1c8d3e
added transfer_used_names;

diff -r b92c2f0413b8 -r 450b1f67f099 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Jul 03 00:40:57 1999 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Jul 04 20:19:28 1999 +0200
@@ -54,6 +54,7 @@
     -> context -> context * ((string * thm list) * thm list)
   val fix: (string * string option) list -> context -> context
   val fix_i: (string * typ) list -> context -> context
+  val transfer_used_names: context -> context -> context
   val setup: (theory -> theory) list
 end;
 
@@ -686,6 +687,12 @@
 val fix_i = gen_fixs cert_typ false;
 
 
+(* transfer_used_names *)
+
+fun transfer_used_names (Context {asms = (_, (_, names)), defs = (_, _, _, used), ...}) =
+  map_context (fn (thy, data, (asms, (fixes, _)), binds, thms, (types, sorts, maxidx, _)) =>
+    (thy, data, (asms, (fixes, names)), binds, thms, (types, sorts, maxidx, used)));
+
 
 (** theory setup **)