--- a/src/HOL/Import/import_package.ML Mon Sep 26 19:19:13 2005 +0200
+++ b/src/HOL/Import/import_package.ML Mon Sep 26 19:19:14 2005 +0200
@@ -54,7 +54,7 @@
val prew = ProofKernel.rewrite_hol4_term prem thy
val prem' = #2 (Logic.dest_equals (prop_of prew))
val _ = message ("Import proved " ^ (string_of_thm thm))
- val thm = Drule.disambiguate_frees thm
+ val thm = ProofKernel.disambiguate_frees thm
val _ = message ("Disambiguate: " ^ (string_of_thm thm))
in
case Shuffler.set_prop thy prem' [("",thm)] of
--- 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 " ^
--- a/src/Pure/drule.ML Mon Sep 26 19:19:13 2005 +0200
+++ b/src/Pure/drule.ML Mon Sep 26 19:19:14 2005 +0200
@@ -149,7 +149,6 @@
val abs_def: thm -> thm
val read_instantiate_sg': theory -> (indexname * string) list -> thm -> thm
val read_instantiate': (indexname * string) list -> thm -> thm
- val disambiguate_frees : thm -> thm
end;
structure Drule: DRULE =
@@ -1146,58 +1145,6 @@
end;
-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
-
end;
structure BasicDrule: BASIC_DRULE = Drule;