src/Pure/Isar/proof_context.ML
changeset 6895 450b1f67f099
parent 6875 df31250ccb3a
child 6931 bd8aa6ae6bcd
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sat Jul 03 00:40:57 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Jul 04 20:19:28 1999 +0200
     1.3 @@ -54,6 +54,7 @@
     1.4      -> context -> context * ((string * thm list) * thm list)
     1.5    val fix: (string * string option) list -> context -> context
     1.6    val fix_i: (string * typ) list -> context -> context
     1.7 +  val transfer_used_names: context -> context -> context
     1.8    val setup: (theory -> theory) list
     1.9  end;
    1.10  
    1.11 @@ -686,6 +687,12 @@
    1.12  val fix_i = gen_fixs cert_typ false;
    1.13  
    1.14  
    1.15 +(* transfer_used_names *)
    1.16 +
    1.17 +fun transfer_used_names (Context {asms = (_, (_, names)), defs = (_, _, _, used), ...}) =
    1.18 +  map_context (fn (thy, data, (asms, (fixes, _)), binds, thms, (types, sorts, maxidx, _)) =>
    1.19 +    (thy, data, (asms, (fixes, names)), binds, thms, (types, sorts, maxidx, used)));
    1.20 +
    1.21  
    1.22  (** theory setup **)
    1.23