src/Pure/pure_thy.ML

 
 (*beware of proper order of evaluation!*)
 
 fun lookup_thms thy =
   let
-    val thy_ref = Theory.self_ref thy;
     val (space, thms) = #theorems (get_theorems thy);
+    val thy_ref = Theory.check_thy thy;
   in
     fn name =>
       Option.map (map (Thm.transfer (Theory.deref thy_ref)))     (*dynamic identity*)
       (Symtab.lookup thms (NameSpace.intern space name)) (*static content*)
   end;