src/HOL/Tools/choice_specification.ML

                 fun remove_alls frees thm =
                     fold (inst_all (Thm.theory_of_thm thm)) frees thm
                 fun process_single ((name,atts),rew_imp,frees) args =
                     let
                         fun undo_imps thm =
-                            equal_elim (symmetric rew_imp) thm
+                            Thm.equal_elim (Thm.symmetric rew_imp) thm
 
                         fun add_final (arg as (thy, thm)) =
                             if name = ""
                             then arg |> Library.swap
                             else (writeln ("  " ^ name ^ ": " ^ Display.string_of_thm_global thy thm);