# HG changeset patch
# User obua
# Date 1127693204 -7200
# Node ID 7e417a7cbf9f5b65262ccad0878dbdede478ab9e
# Parent  e063c0403650087d147fbbcb0d262cf52f822375
added Drule.disambiguate_frees : thm -> thm

diff -r e063c0403650 -r 7e417a7cbf9f src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sun Sep 25 23:36:14 2005 +0200
+++ b/src/Pure/drule.ML	Mon Sep 26 02:06:44 2005 +0200
@@ -149,6 +149,7 @@
   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 =
@@ -1145,6 +1146,58 @@
 
 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;