src/HOL/Topological_Spaces.thy

       val mp_thms = thms RL [@{thm eventually_rev_mp}]
       val raw_elim_thm =
         (@{thm allI} RS @{thm always_eventually})
         |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
         |> fold (fn _ => fn thm => @{thm impI} RS thm) thms
-      val cases_prop = prop_of (raw_elim_thm RS st)
+      val cases_prop = Thm.prop_of (raw_elim_thm RS st)
       val cases = (Rule_Cases.make_common (thy, cases_prop) [(("elim", []), [])])
     in
       CASES cases (rtac raw_elim_thm 1)
     end) 1
 *}