src/HOL/Tools/BNF/bnf_def.ML

                 ((b, NoSyn), ((Thm.def_binding b, []), rhs)) lthy)
           end
       end;
 
     fun maybe_restore lthy_old lthy =
-      lthy |> not (Theory.eq_thy (apply2 Proof_Context.theory_of (lthy_old, lthy)))
+      lthy |> not (Context.eq_thy (apply2 Proof_Context.theory_of (lthy_old, lthy)))
         ? Local_Theory.restore;
 
     val map_bind_def =
       (fn () => def_qualify (if Binding.is_empty map_b then mk_prefix_binding mapN else map_b),
          map_rhs);