src/Tools/code/code_package.ML

         val vars = Term.add_frees t [];
         val tfrees2 = fold (Term.add_tfreesT o snd) vars [];
         val tfrees' = subtract (op =) tfrees2 tfrees1 |> map TFree;
         val ty = map Term.itselfT tfrees' @ map snd vars ---> ty_judg;
         val tfree_vars = map Logic.mk_type tfrees';
-        val c = PureThy.string_of_thmref thmref
+        val c = Facts.string_of_ref thmref
           |> NameSpace.explode
           |> (fn [x] => [x] | (x::xs) => xs)
           |> space_implode "_"
         val propdef = (((c, ty), tfree_vars @ map Free vars), t);
       in if c = "" then NONE else SOME (thmref, propdef) end;
   in
     Facts.dest (PureThy.all_facts_of thy)
-    |> maps PureThy.selections
+    |> maps Facts.selections
     |> map_filter select
     |> map_filter mk_codeprop
   end;
 
 fun add_codeprops all_cs sel_cs thy =
   let
     val codeprops = mk_codeprops thy all_cs sel_cs;
     fun lift_name_yield f x = (Name.context, x) |> f ||> snd;
     fun add (thmref, (((raw_c, ty), ts), t)) (names, thy) =
       let
-        val _ = warning ("Adding theorem " ^ quote (PureThy.string_of_thmref thmref)
+        val _ = warning ("Adding theorem " ^ quote (Facts.string_of_ref thmref)
           ^ " as code property " ^ quote raw_c);
         val ([raw_c'], names') = Name.variants [raw_c] names;
         val (const as Const (c, _), thy') = thy |> Sign.declare_const [] (raw_c', ty, NoSyn);
         val eq = Logic.mk_equals (list_comb (const, ts), t);
         val ([def], thy'') = thy' |> PureThy.add_defs_i false [((Thm.def_name raw_c', eq), [])];