diff -r e7ee815b04bf -r feebdaa346e5 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Sun Nov 15 07:17:05 2020 +0000
+++ b/src/HOL/Library/Float.thy	Sun Nov 15 07:17:06 2020 +0000
@@ -318,9 +318,15 @@
 
 end
 
-definition (in term_syntax) [code_unfold]:
+context
+  includes term_syntax
+begin
+
+definition [code_unfold]:
   "valtermify_float x y = Code_Evaluation.valtermify Float {\<cdot>} x {\<cdot>} y"
 
+end
+
 instantiation float :: full_exhaustive
 begin