--- a/src/HOL/Import/proof_kernel.ML Mon Sep 26 19:19:13 2005 +0200
+++ b/src/HOL/Import/proof_kernel.ML Mon Sep 26 19:19:14 2005 +0200
@@ -53,6 +53,7 @@
exception PK of string * string
val get_proof_dir: string -> theory -> string option
+ val disambiguate_frees : Thm.thm -> Thm.thm
val debug : bool ref
val disk_info_of : proof -> (string * string) option
val set_disk_info_of : proof -> string -> string -> unit
@@ -1119,6 +1120,58 @@
(* End of disambiguating code *)
+fun disambiguate_frees thm =
+ let
+ fun ERR s = error ("Drule.disambiguate_frees: "^s)
+ val ct = cprop_of thm
+ val t = term_of ct
+ val thy = theory_of_cterm ct
+ val frees = term_frees t
+ val freenames = add_term_free_names (t, [])
+ fun is_old_name n = n mem_string freenames
+ fun name_of (Free (n, _)) = n
+ | name_of _ = ERR "name_of"
+ fun new_name' bump map n =
+ let val n' = n^bump in
+ if is_old_name n' orelse Symtab.lookup map n' <> NONE then
+ new_name' (Symbol.bump_string bump) map n
+ else
+ n'
+ end
+ val new_name = new_name' "a"
+ fun replace_name n' (Free (n, t)) = Free (n', t)
+ | replace_name n' _ = ERR "replace_name"
+ (* map: old oder fresh name -> old free,
+ invmap: old free which has fresh name assigned to it -> fresh name *)
+ fun dis (v, mapping as (map,invmap)) =
+ let val n = name_of v in
+ case Symtab.lookup map n of
+ NONE => (Symtab.update (n, v) map, invmap)
+ | SOME v' =>
+ if v=v' then
+ mapping
+ else
+ let val n' = new_name map n in
+ (Symtab.update (n', v) map,
+ Termtab.update (v, n') invmap)
+ end
+ end
+ in
+ if (length freenames = length frees) then
+ thm
+ else
+ let
+ val (_, invmap) =
+ List.foldl dis (Symtab.empty, Termtab.empty) frees
+ fun make_subst ((oldfree, newname), (intros, elims)) =
+ (cterm_of thy oldfree :: intros,
+ cterm_of thy (replace_name newname oldfree) :: elims)
+ val (intros, elims) = List.foldl make_subst ([], []) (Termtab.dest invmap)
+ in
+ forall_elim_list elims (forall_intr_list intros thm)
+ end
+ end
+
val debug = ref false
fun if_debug f x = if !debug then f x else ()
@@ -1304,7 +1357,7 @@
val rew = rewrite_hol4_term (concl_of th) thy
val th = equal_elim rew th
val thy' = add_hol4_pending thyname thmname args thy
- val th = Drule.disambiguate_frees th
+ val th = disambiguate_frees th
val thy2 = if gen_output
then add_dump ("lemma " ^ (quotename thmname) ^ ": " ^
(smart_string_of_thm th) ^ "\n by (import " ^