# HG changeset patch
# User wenzelm
# Date 1433232766 -7200
# Node ID 88505460fde7a89e9fecb71812ae2f660d82bb9e
# Parent  f585b1f0b4c35b586cff8974bd9d7e05fec0fc33
clarified context;

diff -r f585b1f0b4c3 -r 88505460fde7 src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Tue Jun 02 10:12:29 2015 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Tue Jun 02 10:12:46 2015 +0200
@@ -28,7 +28,7 @@
   (*utility functions*)
   val can_apply : Time.time -> (Proof.context -> int -> tactic) ->
     Proof.state -> bool
-  val theorems_in_proof_term : thm -> thm list
+  val theorems_in_proof_term : theory -> thm -> thm list
   val theorems_of_sucessful_proof : Toplevel.state option -> thm list
   val get_setting : (string * string) list -> string * string -> string
   val get_int_setting : (string * string) list -> string * int -> int
@@ -178,9 +178,9 @@
 
 in
 
-fun theorems_in_proof_term thm =
+fun theorems_in_proof_term thy thm =
   let
-    val all_thms = Global_Theory.all_thms_of (Thm.theory_of_thm thm) true
+    val all_thms = Global_Theory.all_thms_of thy true
     fun collect (s, _, _) = if s <> "" then insert (op =) s else I
     fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE
     fun resolve_thms names = map_filter (member_of names) all_thms
@@ -195,7 +195,8 @@
     NONE => []
   | SOME st =>
       if not (Toplevel.is_proof st) then []
-      else theorems_in_proof_term (#goal (Proof.goal (Toplevel.proof_of st))))
+      else
+        theorems_in_proof_term (Toplevel.theory_of st) (#goal (Proof.goal (Toplevel.proof_of st))))
 
 fun get_setting settings (key, default) =
   the_default default (AList.lookup (op =) settings key)