src/HOL/Tools/Sledgehammer/sledgehammer_util.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jan 04 21:56:19 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jan 04 21:56:20 2013 +0100
@@ -18,7 +18,8 @@
   val parse_time_option : string -> string -> Time.time option
   val subgoal_count : Proof.state -> int
   val reserved_isar_keyword_table : unit -> unit Symtab.table
-  val thms_in_proof : string Symtab.table option -> thm -> string list
+  val thms_in_proof :
+    (string Symtab.table * string Symtab.table) option -> thm -> string list
   val thms_of_name : Proof.context -> string -> thm list
   val one_day : Time.time
   val one_year : Time.time
@@ -86,36 +87,43 @@
 (* 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 thm_name name_map =
+fun fold_body_thms outer_name (map_plain_name, map_inclass_name) =
   let
-    val thm_name' = name_map thm_name
-    fun app n (PBody {thms, ...}) =
+    fun app map_name n (PBody {thms, ...}) =
       thms |> fold (fn (_, (name, _, body)) => fn accum =>
           let
-            val name' = name_map name
-            val collect = union (op =) o the_list
-            (* The "name = thm_name" case caters for the uncommon case where the
-               proved theorem occurs in its own proof (e.g.,
-               "Transitive_Closure.trancl_into_trancl"). The "name' = thm_name'"
-               case is to unfold low-level class facts ("Xxx.yyy.zzz") in the
-               proof of high-level class facts ("XXX.yyy_class.zzz"). *)
-            val no_name =
-              (name = "" orelse
-               (n = 1 andalso (name = thm_name orelse name' = thm_name')))
+            val collect = union (op =) o the_list o map_name
+            (* The "name = outer_name" case caters for the uncommon case where
+               the proved theorem occurs in its own proof (e.g.,
+               "Transitive_Closure.trancl_into_trancl"). *)
+            val (anonymous, enter_class) =
+              if name = "" orelse (n = 1 andalso name = outer_name) then
+                (true, false)
+              else if n = 1 andalso map_inclass_name name = SOME outer_name then
+                (true, true)
+              else
+                (false, false)
             val accum =
-              accum |> (if n = 1 andalso not no_name then collect name' else I)
-            val n = n + (if no_name then 0 else 1)
-          in accum |> (if n <= 1 then app n (Future.join body) else I) end)
-  in fold (app 0) end
+              accum |> (if n = 1 andalso not anonymous then collect name else I)
+            val n = n + (if anonymous then 0 else 1)
+          in
+            accum
+            |> (if n <= 1 then
+                  app (if enter_class then map_inclass_name else map_name) n
+                      (Future.join body)
+                else
+                  I)
+          end)
+  in fold (app map_plain_name 0) end
 
-fun thms_in_proof all_names th =
+fun thms_in_proof name_tabs th =
   let
-    val name_map =
-      case all_names of
-        SOME names => Symtab.lookup names
-      | NONE => SOME
+    val map_names =
+      case name_tabs of
+        SOME p => pairself Symtab.lookup p
+      | NONE => `I SOME
     val names =
-      [] |> fold_body_thms (Thm.get_name_hint th) name_map [Thm.proof_body_of th]
+      fold_body_thms (Thm.get_name_hint th) map_names [Thm.proof_body_of th] []
   in names end
 
 fun thms_of_name ctxt name =