src/HOL/Import/proof_kernel.ML

 
             val thy1 = List.foldr (fn(name,thy)=>
                                 snd (get_defname thyname name thy)) thy1 names
             fun new_name name = fst (get_defname thyname name thy1)
             val names' = map (fn name => (new_name name,name,false)) names
-            val (thy',res) = SpecificationPackage.add_specification NONE
+            val (thy',res) = Choice_Specification.add_specification NONE
                                  names'
                                  (thy1,th)
             val _ = ImportRecorder.add_specification names' th
             val res' = Thm.unvarify res
             val hth = HOLThm(rens,res')

             val tfrees = OldTerm.term_tfrees c
             val tnames = map fst tfrees
             val tsyn = mk_syn thy tycname
             val typ = (tycname,tnames,tsyn)
             val ((_, typedef_info), thy') =
-              TypedefPackage.add_typedef false (SOME (Binding.name thmname))
+              Typedef.add_typedef false (SOME (Binding.name thmname))
                 (Binding.name tycname, tnames, tsyn) c NONE (rtac th2 1) thy
             val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
 
             val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
 

             val tfrees = OldTerm.term_tfrees c
             val tnames = sort string_ord (map fst tfrees)
             val tsyn = mk_syn thy tycname
             val typ = (tycname,tnames,tsyn)
             val ((_, typedef_info), thy') =
-              TypedefPackage.add_typedef false NONE (Binding.name tycname,tnames,tsyn) c
+              Typedef.add_typedef false NONE (Binding.name tycname,tnames,tsyn) c
                 (SOME(Binding.name rep_name,Binding.name abs_name)) (rtac th2 1) thy
             val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2
             val fulltyname = Sign.intern_type thy' tycname
             val aty = Type (fulltyname, map mk_vartype tnames)
             val abs_ty = tT --> aty