src/HOL/Import/proof_kernel.ML

         fun mk_res th = HOLThm (rens_of info, Thm.equal_elim i2h_conc th)
     in
         case get_hol4_mapping thyname thmname thy of
             SOME (SOME thmname) =>
             let
-                val th1 = (SOME (PureThy.get_thm thy thmname)
+                val th1 = (SOME (Global_Theory.get_thm thy thmname)
                            handle ERROR _ =>
                                   (case split_name thmname of
-                                       SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy listname,idx-1))
+                                       SOME (listname,idx) => (SOME (List.nth(Global_Theory.get_thms thy listname,idx-1))
                                                                handle _ => NONE)  (* FIXME avoid handle _ *)
                                      | NONE => NONE))
             in
                 case th1 of
                     SOME th2 =>

         val thy1 = case HOL4DefThy.get thy of
                        Replaying _ => thy
                      | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)];
                               Sign.add_consts_i [(Binding.name constname,ctype,csyn)] thy)
         val eq = mk_defeq constname rhs' thy1
-        val (thms, thy2) = PureThy.add_defs false [((Binding.name thmname,eq),[])] thy1
+        val (thms, thy2) = Global_Theory.add_defs false [((Binding.name thmname,eq),[])] thy1
         val _ = ImportRecorder.add_defs thmname eq
         val def_thm = hd thms
         val thm' = def_thm RS meta_eq_to_obj_eq_thm
         val (thy',th) = (thy2, thm')
         val fullcname = Sign.intern_const thy' constname

     end
 
 fun type_introduction thyname thmname tycname abs_name rep_name (P,t) hth thy =
     case HOL4DefThy.get thy of
         Replaying _ => (thy,
-          HOLThm([], PureThy.get_thm thy (thmname^"_@intern")) handle ERROR _ => hth)
+          HOLThm([], Global_Theory.get_thm thy (thmname^"_@intern")) handle ERROR _ => hth)
       | _ =>
         let
             val _ = message "TYPE_INTRO:"
             val _ = if_debug pth hth
             val _ = warning ("Introducing type " ^ tycname ^ " (with morphisms " ^ abs_name ^ " and " ^ rep_name ^ ")")