src/HOL/Mutabelle/mutabelle.ML
changeset 39557 fe5722fce758
parent 37863 7f113caabcf4
child 40132 7ee65dbffa31
--- a/src/HOL/Mutabelle/mutabelle.ML	Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle.ML	Mon Sep 20 16:05:25 2010 +0200
@@ -59,7 +59,7 @@
 
 fun all_unconcealed_thms_of thy =
   let
-    val facts = PureThy.facts_of thy
+    val facts = Global_Theory.facts_of thy
   in
     Facts.fold_static
       (fn (s, ths) =>