# HG changeset patch
# User blanchet
# Date 1308669459 -7200
# Node ID 75caf7e4302e1d39f8571e000ca4509b3955c215
# Parent  a5b1d34d8be781e2b312d6d5c26ca6f6c29e2d77
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")

diff -r a5b1d34d8be7 -r 75caf7e4302e src/HOL/ex/atp_export.ML
--- a/src/HOL/ex/atp_export.ML	Tue Jun 21 17:17:39 2011 +0200
+++ b/src/HOL/ex/atp_export.ML	Tue Jun 21 17:17:39 2011 +0200
@@ -31,7 +31,7 @@
 (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
    fixes that seem to be missing over there; or maybe the two code portions are
    not doing the same? *)
-fun fold_body_thms all_names f =
+fun fold_body_thms thm_name all_names f =
   let
     fun app n (PBody {thms, ...}) =
       thms |> fold (fn (_, (name, prop, body)) => fn x =>
@@ -40,7 +40,10 @@
           val n' =
             n + (if name = "" orelse
                     (is_some all_names andalso
-                     not (member (op =) (the all_names) name)) then
+                     not (member (op =) (the all_names) name)) orelse
+                    (* uncommon case where the proved theorem occurs twice
+                       (e.g., "Transitive_Closure.trancl_into_trancl") *)
+                    n = 1 andalso name = thm_name then
                    0
                  else
                    1)
@@ -52,7 +55,8 @@
   let
     fun collect (s, _, _) = if s <> "" then insert (op =) s else I
     val names =
-      [] |> fold_body_thms all_names collect [Thm.proof_body_of thm]
+      [] |> fold_body_thms (Thm.get_name_hint thm) all_names collect
+                           [Thm.proof_body_of thm]
          |> map fact_name_of
   in names end