--- a/src/HOL/Library/code_lazy.ML Tue Sep 21 11:34:58 2021 +0200
+++ b/src/HOL/Library/code_lazy.ML Tue Sep 21 12:08:41 2021 +0200
@@ -91,7 +91,7 @@
val lthy' = (snd o Local_Theory.begin_nested) lthy
val ((t, (_, thm)), lthy') = Specification.definition NONE [] []
((Thm.def_binding (Binding.name name), []), def) lthy'
- val lthy' = Specification.notation true ("", false) [(t, Mixfix.mixfix "_")] lthy'
+ val lthy' = Local_Theory.notation true ("", false) [(t, Mixfix.mixfix "_")] lthy'
val lthy = Local_Theory.end_nested lthy'
val def_thm = singleton (Proof_Context.export lthy' lthy) thm
in