diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Mon Sep 20 16:05:25 2010 +0200
@@ -183,7 +183,7 @@
 
 fun theorems_in_proof_term thm =
   let
-    val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm)
+    val all_thms = Global_Theory.all_thms_of (Thm.theory_of_thm thm)
     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