src/FOL/ex/Locale_Test/Locale_Test1.thy

--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Sep 20 15:29:53 2010 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Sep 20 16:05:25 2010 +0200
@@ -442,7 +442,7 @@
 interpretation int2?: semi "op +"
   by unfold_locales  (* subsumed, thm int2.assoc not generated *)
 
-ML {* (PureThy.get_thms @{theory} "int2.assoc";
+ML {* (Global_Theory.get_thms @{theory} "int2.assoc";
     error "thm int2.assoc was generated")
   handle ERROR "Unknown fact \"int2.assoc\"" => ([]:thm list); *}