--- 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