--- a/src/HOL/Library/FSet.thy Sun Nov 15 07:17:05 2020 +0000
+++ b/src/HOL/Library/FSet.thy Sun Nov 15 07:17:06 2020 +0000
@@ -1314,12 +1314,18 @@
notation Quickcheck_Exhaustive.orelse (infixr "orelse" 55)
-definition (in term_syntax) [code_unfold]:
+context
+ includes term_syntax
+begin
+
+definition [code_unfold]:
"valterm_femptyset = Code_Evaluation.valtermify ({||} :: ('a :: typerep) fset)"
-definition (in term_syntax) [code_unfold]:
+definition [code_unfold]:
"valtermify_finsert x s = Code_Evaluation.valtermify finsert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
+end
+
instantiation fset :: (exhaustive) exhaustive
begin