src/FOL/ex/LocaleTest.thy

 ML {* set show_sorts *}
 
 ML {*
   fun check_thm name = let
     val thy = the_context ();
-    val thm = get_thm thy (Name name);
+    val thm = get_thm thy (Facts.Named (name, NONE));
     val {prop, hyps, ...} = rep_thm thm;
     val prems = Logic.strip_imp_prems prop;
     val _ = if null hyps then ()
         else error ("Theorem " ^ quote name ^ " has meta hyps.\n" ^
           "Consistency check of locales package failed.");