src/HOL/Tools/Function/function.ML

                 tinduct) |> snd
           end
     in
       lthy
       |> ProofContext.note_thmss ""
-         [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd
+         [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd
       |> ProofContext.note_thmss ""
-         [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
+         [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
       |> ProofContext.note_thmss ""
-         [((Binding.name "termination", [ContextRules.intro_bang (SOME 0)]),
+         [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
            [([Goal.norm_result termination], [])])] |> snd
       |> Proof.theorem_i NONE afterqed [[(goal, [])]]
     end
 
 val termination_proof = gen_termination_proof Syntax.check_term;