# HG changeset patch
# User wenzelm
# Date 1662154914 -7200
# Node ID e076b1b42c44a1cbd1b90f2abc1d80ef57f65d98
# Parent  4a1330addb4e518da0f30fbba4646fbea2c00169
tuned;

diff -r 4a1330addb4e -r e076b1b42c44 src/HOL/Examples/Records.thy
--- a/src/HOL/Examples/Records.thy	Fri Sep 02 23:19:02 2022 +0200
+++ b/src/HOL/Examples/Records.thy	Fri Sep 02 23:41:54 2022 +0200
@@ -327,7 +327,7 @@
 text \<open>Normalisation towards an update ordering (string ordering of update function names) can
 be configured as follows.\<close>
 schematic_goal "r\<lparr>b := y, a := x\<rparr> = ?X"
-  supply [[record_sort_updates = true]]
+  supply [[record_sort_updates]]
   by simp
 
 text \<open>Note the interplay between update ordering and record equality. Without update ordering
@@ -347,16 +347,16 @@
 is no need for componentwise comparison.\<close>
 
 lemma "r\<lparr>f := x1, a:= x2\<rparr> = r\<lparr>a := x2, f:= x1\<rparr>"
-  supply [[record_sort_updates = true, simproc del: Record.eq]]
+  supply [[record_sort_updates, simproc del: Record.eq]]
   apply simp
   done
 
 schematic_goal "r\<lparr>f := x1, e := x2, d:= x3, c:= x4, b:=x5, a:= x6\<rparr> = ?X"
-  supply [[record_sort_updates = true]]
+  supply [[record_sort_updates]]
   by simp
 
 schematic_goal "r\<lparr>f := x1, e := x2, d:= x3, c:= x4, e:=x5, a:= x6\<rparr> = ?X"
-  supply [[record_sort_updates = true]]
+  supply [[record_sort_updates]]
   by simp
 
 schematic_goal "r\<lparr>f := x1, e := x2, d:= x3, c:= x4, e:=x5, a:= x6\<rparr> = ?X"
@@ -400,7 +400,7 @@
 end
 \<close>
 
-declare [[record_codegen = true]]
+declare [[record_codegen]]
 
 schematic_goal \<open>fld_1 (r\<lparr>fld_300 := x300, fld_20 := x20, fld_200 := x200\<rparr>) = ?X\<close>
   by simp