src/HOL/Mutabelle/mutabelle_extra.ML

   map_types (map_type_tvar (fn ((a, i), S) =>
     TFree (if i = 0 then a else a ^ "_" ^ string_of_int i, S)))
 
 fun thms_of all thy =
   filter
-    (fn th => (all orelse Context.theory_name (Thm.theory_of_thm th) = Context.theory_name thy)
+    (fn th => (all orelse Thm.theory_name_of_thm th = Context.theory_name thy)
       (* andalso is_executable_thm thy th *))
     (map snd (filter_out is_forbidden_theorem (Global_Theory.all_thms_of thy false)))
 
 fun elapsed_time description e =
   let val ({elapsed, ...}, result) = Timing.timing e ()