merged
authorhaftmann
Mon Dec 21 08:32:22 2009 +0100 (2009-12-21)
changeset 341535da0f7abbe29
parent 34149 a0efb4754cb7
parent 34152 8e5b596d8c73
child 34154 763559e5356b
child 34170 254ac75e4c38
merged
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Fun.thy	Sat Dec 19 09:07:04 2009 -0800
     1.2 +++ b/src/HOL/Fun.thy	Mon Dec 21 08:32:22 2009 +0100
     1.3 @@ -74,6 +74,14 @@
     1.4  lemma o_id [simp]: "f o id = f"
     1.5  by (simp add: comp_def)
     1.6  
     1.7 +lemma o_eq_dest:
     1.8 +  "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
     1.9 +  by (simp only: o_def) (fact fun_cong)
    1.10 +
    1.11 +lemma o_eq_elim:
    1.12 +  "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
    1.13 +  by (erule meta_mp) (fact o_eq_dest) 
    1.14 +
    1.15  lemma image_compose: "(f o g) ` r = f`(g`r)"
    1.16  by (simp add: comp_def, blast)
    1.17  
     2.1 --- a/src/HOL/Record.thy	Sat Dec 19 09:07:04 2009 -0800
     2.2 +++ b/src/HOL/Record.thy	Mon Dec 21 08:32:22 2009 +0100
     2.3 @@ -59,8 +59,8 @@
     2.4    time as the intermediate terms are @{text "O(log(n))"} in size and
     2.5    the types needed have size bounded by K.  To enable this analagous
     2.6    traversal, we define the functions seen below: @{text
     2.7 -  "istuple_fst"}, @{text "istuple_snd"}, @{text "istuple_fst_update"}
     2.8 -  and @{text "istuple_snd_update"}. These functions generalise tuple
     2.9 +  "iso_tuple_fst"}, @{text "iso_tuple_snd"}, @{text "iso_tuple_fst_update"}
    2.10 +  and @{text "iso_tuple_snd_update"}. These functions generalise tuple
    2.11    operations by taking a parameter that encapsulates a tuple
    2.12    isomorphism.  The rewrites needed on these functions now need an
    2.13    additional assumption which is that the isomorphism works.
    2.14 @@ -79,278 +79,259 @@
    2.15  
    2.16  subsection {* Operators and lemmas for types isomorphic to tuples *}
    2.17  
    2.18 -datatype ('a, 'b, 'c) tuple_isomorphism = TupleIsomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a"
    2.19 +datatype ('a, 'b, 'c) tuple_isomorphism = Tuple_Isomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a"
    2.20  
    2.21  primrec repr :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'c" where
    2.22 -  "repr (TupleIsomorphism r a) = r"
    2.23 +  "repr (Tuple_Isomorphism r a) = r"
    2.24  
    2.25  primrec abst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<times> 'c \<Rightarrow> 'a" where
    2.26 -  "abst (TupleIsomorphism r a) = a"
    2.27 +  "abst (Tuple_Isomorphism r a) = a"
    2.28  
    2.29 -definition istuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b" where
    2.30 -  "istuple_fst isom = fst \<circ> repr isom"
    2.31 +definition iso_tuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b" where
    2.32 +  "iso_tuple_fst isom = fst \<circ> repr isom"
    2.33  
    2.34 -definition istuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c" where
    2.35 -  "istuple_snd isom = snd \<circ> repr isom"
    2.36 +definition iso_tuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c" where
    2.37 +  "iso_tuple_snd isom = snd \<circ> repr isom"
    2.38  
    2.39 -definition istuple_fst_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)" where
    2.40 -  "istuple_fst_update isom f = abst isom \<circ> apfst f \<circ> repr isom"
    2.41 +definition iso_tuple_fst_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)" where
    2.42 +  "iso_tuple_fst_update isom f = abst isom \<circ> apfst f \<circ> repr isom"
    2.43  
    2.44 -definition istuple_snd_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)" where
    2.45 -  "istuple_snd_update isom f = abst isom \<circ> apsnd f \<circ> repr isom"
    2.46 +definition iso_tuple_snd_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)" where
    2.47 +  "iso_tuple_snd_update isom f = abst isom \<circ> apsnd f \<circ> repr isom"
    2.48  
    2.49 -definition istuple_cons :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" where
    2.50 -  "istuple_cons isom = curry (abst isom)"
    2.51 +definition iso_tuple_cons :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" where
    2.52 +  "iso_tuple_cons isom = curry (abst isom)"
    2.53  
    2.54  
    2.55  subsection {* Logical infrastructure for records *}
    2.56  
    2.57 -definition istuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
    2.58 -  "istuple_surjective_proof_assist x y f \<longleftrightarrow> f x = y"
    2.59 +definition iso_tuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
    2.60 +  "iso_tuple_surjective_proof_assist x y f \<longleftrightarrow> f x = y"
    2.61  
    2.62 -definition istuple_update_accessor_cong_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
    2.63 -  "istuple_update_accessor_cong_assist upd acc \<longleftrightarrow> 
    2.64 +definition iso_tuple_update_accessor_cong_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
    2.65 +  "iso_tuple_update_accessor_cong_assist upd acc \<longleftrightarrow> 
    2.66       (\<forall>f v. upd (\<lambda>x. f (acc v)) v = upd f v) \<and> (\<forall>v. upd id v = v)"
    2.67  
    2.68 -definition istuple_update_accessor_eq_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
    2.69 -  "istuple_update_accessor_eq_assist upd acc v f v' x \<longleftrightarrow>
    2.70 -     upd f v = v' \<and> acc v = x \<and> istuple_update_accessor_cong_assist upd acc"
    2.71 +definition iso_tuple_update_accessor_eq_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
    2.72 +  "iso_tuple_update_accessor_eq_assist upd acc v f v' x \<longleftrightarrow>
    2.73 +     upd f v = v' \<and> acc v = x \<and> iso_tuple_update_accessor_cong_assist upd acc"
    2.74  
    2.75  lemma update_accessor_congruence_foldE:
    2.76 -  assumes uac: "istuple_update_accessor_cong_assist upd acc"
    2.77 +  assumes uac: "iso_tuple_update_accessor_cong_assist upd acc"
    2.78    and       r: "r = r'" and v: "acc r' = v'"
    2.79    and       f: "\<And>v. v' = v \<Longrightarrow> f v = f' v"
    2.80    shows        "upd f r = upd f' r'"
    2.81    using uac r v [symmetric]
    2.82    apply (subgoal_tac "upd (\<lambda>x. f (acc r')) r' = upd (\<lambda>x. f' (acc r')) r'")
    2.83 -   apply (simp add: istuple_update_accessor_cong_assist_def)
    2.84 +   apply (simp add: iso_tuple_update_accessor_cong_assist_def)
    2.85    apply (simp add: f)
    2.86    done
    2.87  
    2.88  lemma update_accessor_congruence_unfoldE:
    2.89 -  "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> r = r' \<Longrightarrow> acc r' = v' \<Longrightarrow> (\<And>v. v = v' \<Longrightarrow> f v = f' v)
    2.90 +  "iso_tuple_update_accessor_cong_assist upd acc \<Longrightarrow> r = r' \<Longrightarrow> acc r' = v' \<Longrightarrow> (\<And>v. v = v' \<Longrightarrow> f v = f' v)
    2.91       \<Longrightarrow> upd f r = upd f' r'"
    2.92    apply (erule(2) update_accessor_congruence_foldE)
    2.93    apply simp
    2.94    done
    2.95  
    2.96 -lemma istuple_update_accessor_cong_assist_id:
    2.97 -  "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> upd id = id"
    2.98 -  by rule (simp add: istuple_update_accessor_cong_assist_def)
    2.99 +lemma iso_tuple_update_accessor_cong_assist_id:
   2.100 +  "iso_tuple_update_accessor_cong_assist upd acc \<Longrightarrow> upd id = id"
   2.101 +  by rule (simp add: iso_tuple_update_accessor_cong_assist_def)
   2.102  
   2.103  lemma update_accessor_noopE:
   2.104 -  assumes uac: "istuple_update_accessor_cong_assist upd acc"
   2.105 +  assumes uac: "iso_tuple_update_accessor_cong_assist upd acc"
   2.106        and acc: "f (acc x) = acc x"
   2.107    shows        "upd f x = x"
   2.108 -using uac by (simp add: acc istuple_update_accessor_cong_assist_id [OF uac, unfolded id_def]
   2.109 +using uac by (simp add: acc iso_tuple_update_accessor_cong_assist_id [OF uac, unfolded id_def]
   2.110    cong: update_accessor_congruence_unfoldE [OF uac])
   2.111  
   2.112  lemma update_accessor_noop_compE:
   2.113 -  assumes uac: "istuple_update_accessor_cong_assist upd acc"
   2.114 +  assumes uac: "iso_tuple_update_accessor_cong_assist upd acc"
   2.115    assumes acc: "f (acc x) = acc x"
   2.116    shows      "upd (g \<circ> f) x = upd g x"
   2.117    by (simp add: acc cong: update_accessor_congruence_unfoldE[OF uac])
   2.118  
   2.119  lemma update_accessor_cong_assist_idI:
   2.120 -  "istuple_update_accessor_cong_assist id id"
   2.121 -  by (simp add: istuple_update_accessor_cong_assist_def)
   2.122 +  "iso_tuple_update_accessor_cong_assist id id"
   2.123 +  by (simp add: iso_tuple_update_accessor_cong_assist_def)
   2.124  
   2.125  lemma update_accessor_cong_assist_triv:
   2.126 -  "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> istuple_update_accessor_cong_assist upd acc"
   2.127 +  "iso_tuple_update_accessor_cong_assist upd acc \<Longrightarrow> iso_tuple_update_accessor_cong_assist upd acc"
   2.128    by assumption
   2.129  
   2.130  lemma update_accessor_accessor_eqE:
   2.131 -  "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> acc v = x"
   2.132 -  by (simp add: istuple_update_accessor_eq_assist_def)
   2.133 +  "iso_tuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> acc v = x"
   2.134 +  by (simp add: iso_tuple_update_accessor_eq_assist_def)
   2.135  
   2.136  lemma update_accessor_updator_eqE:
   2.137 -  "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> upd f v = v'"
   2.138 -  by (simp add: istuple_update_accessor_eq_assist_def)
   2.139 +  "iso_tuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> upd f v = v'"
   2.140 +  by (simp add: iso_tuple_update_accessor_eq_assist_def)
   2.141  
   2.142 -lemma istuple_update_accessor_eq_assist_idI:
   2.143 -  "v' = f v \<Longrightarrow> istuple_update_accessor_eq_assist id id v f v' v"
   2.144 -  by (simp add: istuple_update_accessor_eq_assist_def update_accessor_cong_assist_idI)
   2.145 +lemma iso_tuple_update_accessor_eq_assist_idI:
   2.146 +  "v' = f v \<Longrightarrow> iso_tuple_update_accessor_eq_assist id id v f v' v"
   2.147 +  by (simp add: iso_tuple_update_accessor_eq_assist_def update_accessor_cong_assist_idI)
   2.148  
   2.149 -lemma istuple_update_accessor_eq_assist_triv:
   2.150 -  "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> istuple_update_accessor_eq_assist upd acc v f v' x"
   2.151 +lemma iso_tuple_update_accessor_eq_assist_triv:
   2.152 +  "iso_tuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> iso_tuple_update_accessor_eq_assist upd acc v f v' x"
   2.153    by assumption
   2.154  
   2.155 -lemma istuple_update_accessor_cong_from_eq:
   2.156 -  "istuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> istuple_update_accessor_cong_assist upd acc"
   2.157 -  by (simp add: istuple_update_accessor_eq_assist_def)
   2.158 -
   2.159 -lemma o_eq_dest:
   2.160 -  "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
   2.161 -  apply (clarsimp simp: o_def)
   2.162 -  apply (erule fun_cong)
   2.163 -  done
   2.164 +lemma iso_tuple_update_accessor_cong_from_eq:
   2.165 +  "iso_tuple_update_accessor_eq_assist upd acc v f v' x \<Longrightarrow> iso_tuple_update_accessor_cong_assist upd acc"
   2.166 +  by (simp add: iso_tuple_update_accessor_eq_assist_def)
   2.167  
   2.168 -lemma o_eq_elim:
   2.169 -  "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
   2.170 -  apply (erule meta_mp)
   2.171 -  apply (erule o_eq_dest)
   2.172 -  done
   2.173 +lemma iso_tuple_surjective_proof_assistI:
   2.174 +  "f x = y \<Longrightarrow> iso_tuple_surjective_proof_assist x y f"
   2.175 +  by (simp add: iso_tuple_surjective_proof_assist_def)
   2.176  
   2.177 -lemma istuple_surjective_proof_assistI:
   2.178 -  "f x = y \<Longrightarrow> istuple_surjective_proof_assist x y f"
   2.179 -  by (simp add: istuple_surjective_proof_assist_def)
   2.180 -
   2.181 -lemma istuple_surjective_proof_assist_idE:
   2.182 -  "istuple_surjective_proof_assist x y id \<Longrightarrow> x = y"
   2.183 -  by (simp add: istuple_surjective_proof_assist_def)
   2.184 +lemma iso_tuple_surjective_proof_assist_idE:
   2.185 +  "iso_tuple_surjective_proof_assist x y id \<Longrightarrow> x = y"
   2.186 +  by (simp add: iso_tuple_surjective_proof_assist_def)
   2.187  
   2.188  locale isomorphic_tuple =
   2.189    fixes isom :: "('a, 'b, 'c) tuple_isomorphism"
   2.190 -    and repr and abst
   2.191 -  defines "repr \<equiv> Record.repr isom"
   2.192 -  defines "abst \<equiv> Record.abst isom"
   2.193 -  assumes repr_inv: "\<And>x. abst (repr x) = x"
   2.194 -  assumes abst_inv: "\<And>y. repr (abst y) = y"
   2.195 +  assumes repr_inv: "\<And>x. abst isom (repr isom x) = x"
   2.196 +  assumes abst_inv: "\<And>y. repr isom (abst isom y) = y"
   2.197  begin
   2.198  
   2.199  lemma repr_inj:
   2.200 -  "repr x = repr y \<longleftrightarrow> x = y"
   2.201 -  apply (rule iffI, simp_all)
   2.202 -  apply (drule_tac f=abst in arg_cong, simp add: repr_inv)
   2.203 -  done
   2.204 +  "repr isom x = repr isom y \<longleftrightarrow> x = y"
   2.205 +  by (auto dest: arg_cong [of "repr isom x" "repr isom y" "abst isom"] simp add: repr_inv)
   2.206  
   2.207  lemma abst_inj:
   2.208 -  "abst x = abst y \<longleftrightarrow> x = y"
   2.209 -  apply (rule iffI, simp_all)
   2.210 -  apply (drule_tac f=repr in arg_cong, simp add: abst_inv)
   2.211 -  done
   2.212 +  "abst isom x = abst isom y \<longleftrightarrow> x = y"
   2.213 +  by (auto dest: arg_cong [of "abst isom x" "abst isom y" "repr isom"] simp add: abst_inv)
   2.214 +
   2.215 +lemmas simps = Let_def repr_inv abst_inv repr_inj abst_inj
   2.216  
   2.217 -lemmas simps = Let_def repr_inv abst_inv repr_inj abst_inj repr_def [symmetric] abst_def [symmetric]
   2.218 -
   2.219 -lemma istuple_access_update_fst_fst:
   2.220 +lemma iso_tuple_access_update_fst_fst:
   2.221    "f o h g = j o f \<Longrightarrow>
   2.222 -    (f o istuple_fst isom) o (istuple_fst_update isom o h) g
   2.223 -          = j o (f o istuple_fst isom)"
   2.224 -  by (clarsimp simp: istuple_fst_update_def istuple_fst_def simps
   2.225 +    (f o iso_tuple_fst isom) o (iso_tuple_fst_update isom o h) g
   2.226 +          = j o (f o iso_tuple_fst isom)"
   2.227 +  by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_fst_def simps
   2.228               intro!: ext elim!: o_eq_elim)
   2.229  
   2.230 -lemma istuple_access_update_snd_snd:
   2.231 +lemma iso_tuple_access_update_snd_snd:
   2.232    "f o h g = j o f \<Longrightarrow>
   2.233 -    (f o istuple_snd isom) o (istuple_snd_update isom o h) g
   2.234 -          = j o (f o istuple_snd isom)"
   2.235 -  by (clarsimp simp: istuple_snd_update_def istuple_snd_def simps
   2.236 +    (f o iso_tuple_snd isom) o (iso_tuple_snd_update isom o h) g
   2.237 +          = j o (f o iso_tuple_snd isom)"
   2.238 +  by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_snd_def simps
   2.239               intro!: ext elim!: o_eq_elim)
   2.240  
   2.241 -lemma istuple_access_update_fst_snd:
   2.242 -  "(f o istuple_fst isom) o (istuple_snd_update isom o h) g
   2.243 -          = id o (f o istuple_fst isom)"
   2.244 -  by (clarsimp simp: istuple_snd_update_def istuple_fst_def simps
   2.245 +lemma iso_tuple_access_update_fst_snd:
   2.246 +  "(f o iso_tuple_fst isom) o (iso_tuple_snd_update isom o h) g
   2.247 +          = id o (f o iso_tuple_fst isom)"
   2.248 +  by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_fst_def simps
   2.249               intro!: ext elim!: o_eq_elim)
   2.250  
   2.251 -lemma istuple_access_update_snd_fst:
   2.252 -  "(f o istuple_snd isom) o (istuple_fst_update isom o h) g
   2.253 -          = id o (f o istuple_snd isom)"
   2.254 -  by (clarsimp simp: istuple_fst_update_def istuple_snd_def simps
   2.255 +lemma iso_tuple_access_update_snd_fst:
   2.256 +  "(f o iso_tuple_snd isom) o (iso_tuple_fst_update isom o h) g
   2.257 +          = id o (f o iso_tuple_snd isom)"
   2.258 +  by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_def simps
   2.259               intro!: ext elim!: o_eq_elim)
   2.260  
   2.261 -lemma istuple_update_swap_fst_fst:
   2.262 +lemma iso_tuple_update_swap_fst_fst:
   2.263    "h f o j g = j g o h f \<Longrightarrow>
   2.264 -    (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
   2.265 -          = (istuple_fst_update isom o j) g o (istuple_fst_update isom o h) f"
   2.266 -  by (clarsimp simp: istuple_fst_update_def simps apfst_compose intro!: ext)
   2.267 +    (iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g
   2.268 +          = (iso_tuple_fst_update isom o j) g o (iso_tuple_fst_update isom o h) f"
   2.269 +  by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose intro!: ext)
   2.270  
   2.271 -lemma istuple_update_swap_snd_snd:
   2.272 +lemma iso_tuple_update_swap_snd_snd:
   2.273    "h f o j g = j g o h f \<Longrightarrow>
   2.274 -    (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
   2.275 -          = (istuple_snd_update isom o j) g o (istuple_snd_update isom o h) f"
   2.276 -  by (clarsimp simp: istuple_snd_update_def simps apsnd_compose intro!: ext)
   2.277 +    (iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g
   2.278 +          = (iso_tuple_snd_update isom o j) g o (iso_tuple_snd_update isom o h) f"
   2.279 +  by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose intro!: ext)
   2.280  
   2.281 -lemma istuple_update_swap_fst_snd:
   2.282 -  "(istuple_snd_update isom o h) f o (istuple_fst_update isom o j) g
   2.283 -          = (istuple_fst_update isom o j) g o (istuple_snd_update isom o h) f"
   2.284 -  by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps intro!: ext)
   2.285 +lemma iso_tuple_update_swap_fst_snd:
   2.286 +  "(iso_tuple_snd_update isom o h) f o (iso_tuple_fst_update isom o j) g
   2.287 +          = (iso_tuple_fst_update isom o j) g o (iso_tuple_snd_update isom o h) f"
   2.288 +  by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def simps intro!: ext)
   2.289  
   2.290 -lemma istuple_update_swap_snd_fst:
   2.291 -  "(istuple_fst_update isom o h) f o (istuple_snd_update isom o j) g
   2.292 -          = (istuple_snd_update isom o j) g o (istuple_fst_update isom o h) f"
   2.293 -  by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps intro!: ext)
   2.294 +lemma iso_tuple_update_swap_snd_fst:
   2.295 +  "(iso_tuple_fst_update isom o h) f o (iso_tuple_snd_update isom o j) g
   2.296 +          = (iso_tuple_snd_update isom o j) g o (iso_tuple_fst_update isom o h) f"
   2.297 +  by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def simps intro!: ext)
   2.298  
   2.299 -lemma istuple_update_compose_fst_fst:
   2.300 +lemma iso_tuple_update_compose_fst_fst:
   2.301    "h f o j g = k (f o g) \<Longrightarrow>
   2.302 -    (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g
   2.303 -          = (istuple_fst_update isom o k) (f o g)"
   2.304 -  by (clarsimp simp: istuple_fst_update_def simps apfst_compose intro!: ext)
   2.305 +    (iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g
   2.306 +          = (iso_tuple_fst_update isom o k) (f o g)"
   2.307 +  by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose intro!: ext)
   2.308  
   2.309 -lemma istuple_update_compose_snd_snd:
   2.310 +lemma iso_tuple_update_compose_snd_snd:
   2.311    "h f o j g = k (f o g) \<Longrightarrow>
   2.312 -    (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g
   2.313 -          = (istuple_snd_update isom o k) (f o g)"
   2.314 -  by (clarsimp simp: istuple_snd_update_def simps apsnd_compose intro!: ext)
   2.315 +    (iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g
   2.316 +          = (iso_tuple_snd_update isom o k) (f o g)"
   2.317 +  by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose intro!: ext)
   2.318  
   2.319 -lemma istuple_surjective_proof_assist_step:
   2.320 -  "istuple_surjective_proof_assist v a (istuple_fst isom o f) \<Longrightarrow>
   2.321 -     istuple_surjective_proof_assist v b (istuple_snd isom o f)
   2.322 -      \<Longrightarrow> istuple_surjective_proof_assist v (istuple_cons isom a b) f"
   2.323 -  by (clarsimp simp: istuple_surjective_proof_assist_def simps
   2.324 -    istuple_fst_def istuple_snd_def istuple_cons_def)
   2.325 +lemma iso_tuple_surjective_proof_assist_step:
   2.326 +  "iso_tuple_surjective_proof_assist v a (iso_tuple_fst isom o f) \<Longrightarrow>
   2.327 +     iso_tuple_surjective_proof_assist v b (iso_tuple_snd isom o f)
   2.328 +      \<Longrightarrow> iso_tuple_surjective_proof_assist v (iso_tuple_cons isom a b) f"
   2.329 +  by (clarsimp simp: iso_tuple_surjective_proof_assist_def simps
   2.330 +    iso_tuple_fst_def iso_tuple_snd_def iso_tuple_cons_def)
   2.331  
   2.332 -lemma istuple_fst_update_accessor_cong_assist:
   2.333 -  assumes "istuple_update_accessor_cong_assist f g"
   2.334 -  shows "istuple_update_accessor_cong_assist (istuple_fst_update isom o f) (g o istuple_fst isom)"
   2.335 +lemma iso_tuple_fst_update_accessor_cong_assist:
   2.336 +  assumes "iso_tuple_update_accessor_cong_assist f g"
   2.337 +  shows "iso_tuple_update_accessor_cong_assist (iso_tuple_fst_update isom o f) (g o iso_tuple_fst isom)"
   2.338  proof -
   2.339 -  from assms have "f id = id" by (rule istuple_update_accessor_cong_assist_id)
   2.340 -  with assms show ?thesis by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
   2.341 -    istuple_fst_update_def istuple_fst_def)
   2.342 +  from assms have "f id = id" by (rule iso_tuple_update_accessor_cong_assist_id)
   2.343 +  with assms show ?thesis by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps
   2.344 +    iso_tuple_fst_update_def iso_tuple_fst_def)
   2.345  qed
   2.346  
   2.347 -lemma istuple_snd_update_accessor_cong_assist:
   2.348 -  assumes "istuple_update_accessor_cong_assist f g"
   2.349 -  shows "istuple_update_accessor_cong_assist (istuple_snd_update isom o f) (g o istuple_snd isom)"
   2.350 +lemma iso_tuple_snd_update_accessor_cong_assist:
   2.351 +  assumes "iso_tuple_update_accessor_cong_assist f g"
   2.352 +  shows "iso_tuple_update_accessor_cong_assist (iso_tuple_snd_update isom o f) (g o iso_tuple_snd isom)"
   2.353  proof -
   2.354 -  from assms have "f id = id" by (rule istuple_update_accessor_cong_assist_id)
   2.355 -  with assms show ?thesis by (clarsimp simp: istuple_update_accessor_cong_assist_def simps
   2.356 -    istuple_snd_update_def istuple_snd_def)
   2.357 +  from assms have "f id = id" by (rule iso_tuple_update_accessor_cong_assist_id)
   2.358 +  with assms show ?thesis by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps
   2.359 +    iso_tuple_snd_update_def iso_tuple_snd_def)
   2.360  qed
   2.361  
   2.362 -lemma istuple_fst_update_accessor_eq_assist:
   2.363 -  assumes "istuple_update_accessor_eq_assist f g a u a' v"
   2.364 -  shows "istuple_update_accessor_eq_assist (istuple_fst_update isom o f) (g o istuple_fst isom)
   2.365 -    (istuple_cons isom a b) u (istuple_cons isom a' b) v"
   2.366 +lemma iso_tuple_fst_update_accessor_eq_assist:
   2.367 +  assumes "iso_tuple_update_accessor_eq_assist f g a u a' v"
   2.368 +  shows "iso_tuple_update_accessor_eq_assist (iso_tuple_fst_update isom o f) (g o iso_tuple_fst isom)
   2.369 +    (iso_tuple_cons isom a b) u (iso_tuple_cons isom a' b) v"
   2.370  proof -
   2.371    from assms have "f id = id"
   2.372 -    by (auto simp add: istuple_update_accessor_eq_assist_def intro: istuple_update_accessor_cong_assist_id)
   2.373 -  with assms show ?thesis by (clarsimp simp: istuple_update_accessor_eq_assist_def
   2.374 -    istuple_fst_update_def istuple_fst_def istuple_update_accessor_cong_assist_def istuple_cons_def simps)
   2.375 +    by (auto simp add: iso_tuple_update_accessor_eq_assist_def intro: iso_tuple_update_accessor_cong_assist_id)
   2.376 +  with assms show ?thesis by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def
   2.377 +    iso_tuple_fst_update_def iso_tuple_fst_def iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps)
   2.378  qed
   2.379  
   2.380 -lemma istuple_snd_update_accessor_eq_assist:
   2.381 -  assumes "istuple_update_accessor_eq_assist f g b u b' v"
   2.382 -  shows "istuple_update_accessor_eq_assist (istuple_snd_update isom o f) (g o istuple_snd isom)
   2.383 -    (istuple_cons isom a b) u (istuple_cons isom a b') v"
   2.384 +lemma iso_tuple_snd_update_accessor_eq_assist:
   2.385 +  assumes "iso_tuple_update_accessor_eq_assist f g b u b' v"
   2.386 +  shows "iso_tuple_update_accessor_eq_assist (iso_tuple_snd_update isom o f) (g o iso_tuple_snd isom)
   2.387 +    (iso_tuple_cons isom a b) u (iso_tuple_cons isom a b') v"
   2.388  proof -
   2.389    from assms have "f id = id"
   2.390 -    by (auto simp add: istuple_update_accessor_eq_assist_def intro: istuple_update_accessor_cong_assist_id)
   2.391 -  with assms show ?thesis by (clarsimp simp: istuple_update_accessor_eq_assist_def
   2.392 -    istuple_snd_update_def istuple_snd_def istuple_update_accessor_cong_assist_def istuple_cons_def simps)
   2.393 +    by (auto simp add: iso_tuple_update_accessor_eq_assist_def intro: iso_tuple_update_accessor_cong_assist_id)
   2.394 +  with assms show ?thesis by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def
   2.395 +    iso_tuple_snd_update_def iso_tuple_snd_def iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps)
   2.396  qed
   2.397  
   2.398 -lemma istuple_cons_conj_eqI:
   2.399 +lemma iso_tuple_cons_conj_eqI:
   2.400    "a = c \<and> b = d \<and> P \<longleftrightarrow> Q \<Longrightarrow>
   2.401 -    istuple_cons isom a b = istuple_cons isom c d \<and> P \<longleftrightarrow> Q"
   2.402 -  by (clarsimp simp: istuple_cons_def simps)
   2.403 +    iso_tuple_cons isom a b = iso_tuple_cons isom c d \<and> P \<longleftrightarrow> Q"
   2.404 +  by (clarsimp simp: iso_tuple_cons_def simps)
   2.405  
   2.406  lemmas intros =
   2.407 -    istuple_access_update_fst_fst
   2.408 -    istuple_access_update_snd_snd
   2.409 -    istuple_access_update_fst_snd
   2.410 -    istuple_access_update_snd_fst
   2.411 -    istuple_update_swap_fst_fst
   2.412 -    istuple_update_swap_snd_snd
   2.413 -    istuple_update_swap_fst_snd
   2.414 -    istuple_update_swap_snd_fst
   2.415 -    istuple_update_compose_fst_fst
   2.416 -    istuple_update_compose_snd_snd
   2.417 -    istuple_surjective_proof_assist_step
   2.418 -    istuple_fst_update_accessor_eq_assist
   2.419 -    istuple_snd_update_accessor_eq_assist
   2.420 -    istuple_fst_update_accessor_cong_assist
   2.421 -    istuple_snd_update_accessor_cong_assist
   2.422 -    istuple_cons_conj_eqI
   2.423 +    iso_tuple_access_update_fst_fst
   2.424 +    iso_tuple_access_update_snd_snd
   2.425 +    iso_tuple_access_update_fst_snd
   2.426 +    iso_tuple_access_update_snd_fst
   2.427 +    iso_tuple_update_swap_fst_fst
   2.428 +    iso_tuple_update_swap_snd_snd
   2.429 +    iso_tuple_update_swap_fst_snd
   2.430 +    iso_tuple_update_swap_snd_fst
   2.431 +    iso_tuple_update_compose_fst_fst
   2.432 +    iso_tuple_update_compose_snd_snd
   2.433 +    iso_tuple_surjective_proof_assist_step
   2.434 +    iso_tuple_fst_update_accessor_eq_assist
   2.435 +    iso_tuple_snd_update_accessor_eq_assist
   2.436 +    iso_tuple_fst_update_accessor_cong_assist
   2.437 +    iso_tuple_snd_update_accessor_cong_assist
   2.438 +    iso_tuple_cons_conj_eqI
   2.439  
   2.440  end
   2.441  
   2.442 @@ -358,29 +339,32 @@
   2.443    fixes repr abst
   2.444    assumes repr_inj: "\<And>x y. repr x = repr y \<longleftrightarrow> x = y"
   2.445       and abst_inv: "\<And>z. repr (abst z) = z"
   2.446 -  assumes v: "v \<equiv> TupleIsomorphism repr abst"
   2.447 +  assumes v: "v \<equiv> Tuple_Isomorphism repr abst"
   2.448    shows "isomorphic_tuple v"
   2.449 -  apply (rule isomorphic_tuple.intro)
   2.450 -  apply (simp_all add: abst_inv v)
   2.451 -  apply (cut_tac x="abst (repr x)" and y="x" in repr_inj)
   2.452 -  apply (simp add: abst_inv)
   2.453 -  done
   2.454 +proof
   2.455 +  have "\<And>x. repr (abst (repr x)) = repr x"
   2.456 +    by (simp add: abst_inv)
   2.457 +  then show "\<And>x. Record.abst v (Record.repr v x) = x"
   2.458 +    by (simp add: v repr_inj)
   2.459 +  show P: "\<And>y. Record.repr v (Record.abst v y) = y"
   2.460 +    by (simp add: v) (fact abst_inv)
   2.461 +qed
   2.462  
   2.463  definition
   2.464 -  "tuple_istuple \<equiv> TupleIsomorphism id id"
   2.465 +  "tuple_iso_tuple \<equiv> Tuple_Isomorphism id id"
   2.466  
   2.467 -lemma tuple_istuple:
   2.468 -  "isomorphic_tuple tuple_istuple"
   2.469 -  by (simp add: isomorphic_tuple_intro [OF _ _ reflexive] tuple_istuple_def)
   2.470 +lemma tuple_iso_tuple:
   2.471 +  "isomorphic_tuple tuple_iso_tuple"
   2.472 +  by (simp add: isomorphic_tuple_intro [OF _ _ reflexive] tuple_iso_tuple_def)
   2.473  
   2.474  lemma refl_conj_eq:
   2.475    "Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R"
   2.476    by simp
   2.477  
   2.478 -lemma istuple_UNIV_I: "x \<in> UNIV \<equiv> True"
   2.479 +lemma iso_tuple_UNIV_I: "x \<in> UNIV \<equiv> True"
   2.480    by simp
   2.481  
   2.482 -lemma istuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
   2.483 +lemma iso_tuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
   2.484    by simp
   2.485  
   2.486  lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
   2.487 @@ -437,9 +421,9 @@
   2.488  use "Tools/record.ML"
   2.489  setup Record.setup
   2.490  
   2.491 -hide (open) const TupleIsomorphism repr abst istuple_fst istuple_snd
   2.492 -  istuple_fst_update istuple_snd_update istuple_cons
   2.493 -  istuple_surjective_proof_assist istuple_update_accessor_cong_assist
   2.494 -  istuple_update_accessor_eq_assist tuple_istuple
   2.495 +hide (open) const Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
   2.496 +  iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
   2.497 +  iso_tuple_surjective_proof_assist iso_tuple_update_accessor_cong_assist
   2.498 +  iso_tuple_update_accessor_eq_assist tuple_iso_tuple
   2.499  
   2.500  end
     3.1 --- a/src/HOL/Tools/record.ML	Sat Dec 19 09:07:04 2009 -0800
     3.2 +++ b/src/HOL/Tools/record.ML	Mon Dec 21 08:32:22 2009 +0100
     3.3 @@ -50,24 +50,24 @@
     3.4  end;
     3.5  
     3.6  
     3.7 -signature ISTUPLE_SUPPORT =
     3.8 +signature ISO_TUPLE_SUPPORT =
     3.9  sig
    3.10 -  val add_istuple_type: bstring * string list -> typ * typ -> theory -> (term * term) * theory
    3.11 +  val add_iso_tuple_type: bstring * string list -> typ * typ -> theory -> (term * term) * theory
    3.12    val mk_cons_tuple: term * term -> term
    3.13    val dest_cons_tuple: term -> term * term
    3.14 -  val istuple_intros_tac: int -> tactic
    3.15 +  val iso_tuple_intros_tac: int -> tactic
    3.16    val named_cterm_instantiate: (string * cterm) list -> thm -> thm
    3.17  end;
    3.18  
    3.19 -structure IsTupleSupport: ISTUPLE_SUPPORT =
    3.20 +structure Iso_Tuple_Support: ISO_TUPLE_SUPPORT =
    3.21  struct
    3.22  
    3.23 -val isomN = "_TupleIsom";
    3.24 -
    3.25 -val istuple_intro = @{thm isomorphic_tuple_intro};
    3.26 -val istuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros};
    3.27 -
    3.28 -val tuple_istuple = (@{const_name tuple_istuple}, @{thm tuple_istuple});
    3.29 +val isoN = "_Tuple_Iso";
    3.30 +
    3.31 +val iso_tuple_intro = @{thm isomorphic_tuple_intro};
    3.32 +val iso_tuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros};
    3.33 +
    3.34 +val tuple_iso_tuple = (@{const_name tuple_iso_tuple}, @{thm tuple_iso_tuple});
    3.35  
    3.36  fun named_cterm_instantiate values thm =
    3.37    let
    3.38 @@ -81,10 +81,10 @@
    3.39      cterm_instantiate (map (apfst getvar) values) thm
    3.40    end;
    3.41  
    3.42 -structure IsTupleThms = Theory_Data
    3.43 +structure Iso_Tuple_Thms = Theory_Data
    3.44  (
    3.45    type T = thm Symtab.table;
    3.46 -  val empty = Symtab.make [tuple_istuple];
    3.47 +  val empty = Symtab.make [tuple_iso_tuple];
    3.48    val extend = I;
    3.49    fun merge data = Symtab.merge Thm.eq_thm_prop data;   (* FIXME handle Symtab.DUP ?? *)
    3.50  );
    3.51 @@ -96,7 +96,7 @@
    3.52          val SOME {Rep_inject = rep_inject, Abs_name = absN, abs_type = absT,
    3.53            Abs_inverse = abs_inverse, ...} = Typedef.get_info thy name;
    3.54          val rewrite_rule =
    3.55 -          MetaSimplifier.rewrite_rule [@{thm istuple_UNIV_I}, @{thm istuple_True_simp}];
    3.56 +          MetaSimplifier.rewrite_rule [@{thm iso_tuple_UNIV_I}, @{thm iso_tuple_True_simp}];
    3.57        in
    3.58          (map rewrite_rule [rep_inject, abs_inverse], Const (absN, repT --> absT), absT)
    3.59        end;
    3.60 @@ -112,14 +112,14 @@
    3.61      val prodT = HOLogic.mk_prodT (leftT, rightT);
    3.62      val isomT = Type (@{type_name tuple_isomorphism}, [prodT, leftT, rightT]);
    3.63    in
    3.64 -    Const (@{const_name istuple_cons}, isomT --> leftT --> rightT --> prodT) $
    3.65 -      Const (fst tuple_istuple, isomT) $ left $ right
    3.66 +    Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> prodT) $
    3.67 +      Const (fst tuple_iso_tuple, isomT) $ left $ right
    3.68    end;
    3.69  
    3.70 -fun dest_cons_tuple (Const (@{const_name istuple_cons}, _) $ Const _ $ t $ u) = (t, u)
    3.71 +fun dest_cons_tuple (Const (@{const_name iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u)
    3.72    | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]);
    3.73  
    3.74 -fun add_istuple_type (name, alphas) (leftT, rightT) thy =
    3.75 +fun add_iso_tuple_type (name, alphas) (leftT, rightT) thy =
    3.76    let
    3.77      val repT = HOLogic.mk_prodT (leftT, rightT);
    3.78  
    3.79 @@ -131,39 +131,39 @@
    3.80      (*construct a type and body for the isomorphism constant by
    3.81        instantiating the theorem to which the definition will be applied*)
    3.82      val intro_inst =
    3.83 -      rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] istuple_intro;
    3.84 +      rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] iso_tuple_intro;
    3.85      val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst));
    3.86      val isomT = fastype_of body;
    3.87 -    val isom_bind = Binding.name (name ^ isomN);
    3.88 +    val isom_bind = Binding.name (name ^ isoN);
    3.89      val isom_name = Sign.full_name typ_thy isom_bind;
    3.90      val isom = Const (isom_name, isomT);
    3.91 -    val isom_spec = (Thm.def_name (name ^ isomN), Logic.mk_equals (isom, body));
    3.92 +    val isom_spec = (Thm.def_name (name ^ isoN), Logic.mk_equals (isom, body));
    3.93  
    3.94      val ([isom_def], cdef_thy) =
    3.95        typ_thy
    3.96        |> Sign.add_consts_i [Syntax.no_syn (isom_bind, isomT)]
    3.97        |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)];
    3.98  
    3.99 -    val istuple = isom_def RS (abs_inverse RS (rep_inject RS istuple_intro));
   3.100 -    val cons = Const (@{const_name istuple_cons}, isomT --> leftT --> rightT --> absT);
   3.101 +    val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
   3.102 +    val cons = Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> absT);
   3.103  
   3.104      val thm_thy =
   3.105        cdef_thy
   3.106 -      |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop (isom_name, istuple))
   3.107 +      |> Iso_Tuple_Thms.map (Symtab.insert Thm.eq_thm_prop (isom_name, iso_tuple))
   3.108        |> Sign.parent_path
   3.109        |> Code.add_default_eqn isom_def;
   3.110    in
   3.111      ((isom, cons $ isom), thm_thy)
   3.112    end;
   3.113  
   3.114 -val istuple_intros_tac = resolve_from_net_tac istuple_intros THEN'
   3.115 +val iso_tuple_intros_tac = resolve_from_net_tac iso_tuple_intros THEN'
   3.116    CSUBGOAL (fn (cgoal, i) =>
   3.117      let
   3.118        val thy = Thm.theory_of_cterm cgoal;
   3.119        val goal = Thm.term_of cgoal;
   3.120  
   3.121 -      val isthms = IsTupleThms.get thy;
   3.122 -      fun err s t = raise TERM ("istuple_intros_tac: " ^ s, [t]);
   3.123 +      val isthms = Iso_Tuple_Thms.get thy;
   3.124 +      fun err s t = raise TERM ("iso_tuple_intros_tac: " ^ s, [t]);
   3.125  
   3.126        val goal' = Envir.beta_eta_contract goal;
   3.127        val is =
   3.128 @@ -197,13 +197,13 @@
   3.129  
   3.130  val refl_conj_eq = @{thm refl_conj_eq};
   3.131  
   3.132 -val surject_assistI = @{thm "istuple_surjective_proof_assistI"};
   3.133 -val surject_assist_idE = @{thm "istuple_surjective_proof_assist_idE"};
   3.134 +val surject_assistI = @{thm "iso_tuple_surjective_proof_assistI"};
   3.135 +val surject_assist_idE = @{thm "iso_tuple_surjective_proof_assist_idE"};
   3.136  
   3.137  val updacc_accessor_eqE = @{thm "update_accessor_accessor_eqE"};
   3.138  val updacc_updator_eqE = @{thm "update_accessor_updator_eqE"};
   3.139 -val updacc_eq_idI = @{thm "istuple_update_accessor_eq_assist_idI"};
   3.140 -val updacc_eq_triv = @{thm "istuple_update_accessor_eq_assist_triv"};
   3.141 +val updacc_eq_idI = @{thm "iso_tuple_update_accessor_eq_assist_idI"};
   3.142 +val updacc_eq_triv = @{thm "iso_tuple_update_accessor_eq_assist_triv"};
   3.143  
   3.144  val updacc_foldE = @{thm "update_accessor_congruence_foldE"};
   3.145  val updacc_unfoldE = @{thm "update_accessor_congruence_unfoldE"};
   3.146 @@ -211,7 +211,7 @@
   3.147  val updacc_noop_compE = @{thm "update_accessor_noop_compE"};
   3.148  val updacc_cong_idI = @{thm "update_accessor_cong_assist_idI"};
   3.149  val updacc_cong_triv = @{thm "update_accessor_cong_assist_triv"};
   3.150 -val updacc_cong_from_eq = @{thm "istuple_update_accessor_cong_from_eq"};
   3.151 +val updacc_cong_from_eq = @{thm "iso_tuple_update_accessor_cong_from_eq"};
   3.152  
   3.153  val o_eq_dest = @{thm o_eq_dest};
   3.154  val o_eq_id_dest = @{thm o_eq_id_dest};
   3.155 @@ -1066,7 +1066,7 @@
   3.156            Goal.prove (ProofContext.init thy) [] [] prop
   3.157              (fn _ =>
   3.158                simp_tac defset 1 THEN
   3.159 -              REPEAT_DETERM (IsTupleSupport.istuple_intros_tac 1) THEN
   3.160 +              REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
   3.161                TRY (simp_tac (HOL_ss addsimps id_o_apps) 1));
   3.162          val dest =
   3.163            if is_sel_upd_pair thy acc upd
   3.164 @@ -1089,7 +1089,7 @@
   3.165        Goal.prove (ProofContext.init thy) [] [] prop
   3.166          (fn _ =>
   3.167            simp_tac defset 1 THEN
   3.168 -          REPEAT_DETERM (IsTupleSupport.istuple_intros_tac 1) THEN
   3.169 +          REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
   3.170            TRY (simp_tac (HOL_ss addsimps [id_apply]) 1));
   3.171      val dest = if comp then o_eq_dest_lhs else o_eq_dest;
   3.172    in Drule.standard (othm RS dest) end;
   3.173 @@ -1117,7 +1117,7 @@
   3.174            else swaps_needed us (u :: prev) (Symtab.insert (K true) (cname u, ()) seen) swaps;
   3.175    in swaps_needed upd_funs [] Symtab.empty Symreltab.empty end;
   3.176  
   3.177 -val named_cterm_instantiate = IsTupleSupport.named_cterm_instantiate;
   3.178 +val named_cterm_instantiate = Iso_Tuple_Support.named_cterm_instantiate;
   3.179  
   3.180  fun prove_unfold_defs thy ex_simps ex_simprs prop =
   3.181    let
   3.182 @@ -1222,7 +1222,7 @@
   3.183      Goal.prove (ProofContext.init thy) [] [] prop
   3.184        (fn _ =>
   3.185          simp_tac simpset 1 THEN
   3.186 -        REPEAT_DETERM (IsTupleSupport.istuple_intros_tac 1) THEN
   3.187 +        REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
   3.188          TRY (resolve_tac [updacc_cong_idI] 1))
   3.189    end;
   3.190  
   3.191 @@ -1612,22 +1612,22 @@
   3.192      (*before doing anything else, create the tree of new types
   3.193        that will back the record extension*)
   3.194  
   3.195 -    val mktreeV = Balanced_Tree.make IsTupleSupport.mk_cons_tuple;
   3.196 -
   3.197 -    fun mk_istuple (left, right) (thy, i) =
   3.198 +    val mktreeV = Balanced_Tree.make Iso_Tuple_Support.mk_cons_tuple;
   3.199 +
   3.200 +    fun mk_iso_tuple (left, right) (thy, i) =
   3.201        let
   3.202          val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
   3.203          val nm = suffix suff (Long_Name.base_name name);
   3.204          val ((_, cons), thy') =
   3.205 -          IsTupleSupport.add_istuple_type
   3.206 +          Iso_Tuple_Support.add_iso_tuple_type
   3.207              (nm, alphas_zeta) (fastype_of left, fastype_of right) thy;
   3.208        in
   3.209          (cons $ left $ right, (thy', i + 1))
   3.210        end;
   3.211  
   3.212 -    (*trying to create a 1-element istuple will fail, and is pointless anyway*)
   3.213 -    fun mk_even_istuple [arg] = pair arg
   3.214 -      | mk_even_istuple args = mk_istuple (IsTupleSupport.dest_cons_tuple (mktreeV args));
   3.215 +    (*trying to create a 1-element iso_tuple will fail, and is pointless anyway*)
   3.216 +    fun mk_even_iso_tuple [arg] = pair arg
   3.217 +      | mk_even_iso_tuple args = mk_iso_tuple (Iso_Tuple_Support.dest_cons_tuple (mktreeV args));
   3.218  
   3.219      fun build_meta_tree_type i thy vars more =
   3.220        let val len = length vars in
   3.221 @@ -1637,12 +1637,12 @@
   3.222              fun group16 [] = []
   3.223                | group16 xs = take 16 xs :: group16 (drop 16 xs);
   3.224              val vars' = group16 vars;
   3.225 -            val (composites, (thy', i')) = fold_map mk_even_istuple vars' (thy, i);
   3.226 +            val (composites, (thy', i')) = fold_map mk_even_iso_tuple vars' (thy, i);
   3.227            in
   3.228              build_meta_tree_type i' thy' composites more
   3.229            end
   3.230          else
   3.231 -          let val (term, (thy', _)) = mk_istuple (mktreeV vars, more) (thy, 0)
   3.232 +          let val (term, (thy', _)) = mk_iso_tuple (mktreeV vars, more) (thy, 0)
   3.233            in (term, thy') end
   3.234        end;
   3.235  
   3.236 @@ -1712,7 +1712,7 @@
   3.237              simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
   3.238              REPEAT_DETERM
   3.239                (rtac refl_conj_eq 1 ORELSE
   3.240 -                IsTupleSupport.istuple_intros_tac 1 ORELSE
   3.241 +                Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
   3.242                  rtac refl 1)));
   3.243  
   3.244      val inject = timeit_msg "record extension inject proof:" inject_prf;
   3.245 @@ -1730,7 +1730,7 @@
   3.246          val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE;
   3.247          val tactic1 =
   3.248            simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
   3.249 -          REPEAT_ALL_NEW IsTupleSupport.istuple_intros_tac 1;
   3.250 +          REPEAT_ALL_NEW Iso_Tuple_Support.iso_tuple_intros_tac 1;
   3.251          val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
   3.252          val [halfway] = Seq.list_of (tactic1 start);
   3.253          val [surject] = Seq.list_of (tactic2 (Drule.standard halfway));
   3.254 @@ -1954,7 +1954,7 @@
   3.255  
   3.256      val ext_defs = ext_def :: map #extdef parents;
   3.257  
   3.258 -    (*Theorems from the istuple intros.
   3.259 +    (*Theorems from the iso_tuple intros.
   3.260        This is complex enough to deserve a full comment.
   3.261        By unfolding ext_defs from r_rec0 we create a tree of constructor
   3.262        calls (many of them Pair, but others as well). The introduction
   3.263 @@ -1979,7 +1979,7 @@
   3.264          val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
   3.265          val tactic =
   3.266            simp_tac (HOL_basic_ss addsimps ext_defs) 1 THEN
   3.267 -          REPEAT (IsTupleSupport.istuple_intros_tac 1 ORELSE terminal);
   3.268 +          REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE terminal);
   3.269          val updaccs = Seq.list_of (tactic init_thm);
   3.270        in
   3.271          (updaccs RL [updacc_accessor_eqE],
   3.272 @@ -2207,7 +2207,7 @@
   3.273               [rtac surject_assist_idE 1,
   3.274                simp_tac init_ss 1,
   3.275                REPEAT
   3.276 -                (IsTupleSupport.istuple_intros_tac 1 ORELSE
   3.277 +                (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
   3.278                    (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))])
   3.279        end;
   3.280      val surjective = timeit_msg "record surjective proof:" surjective_prf;
     4.1 --- a/src/Tools/Code/code_printer.ML	Sat Dec 19 09:07:04 2009 -0800
     4.2 +++ b/src/Tools/Code/code_printer.ML	Mon Dec 21 08:32:22 2009 +0100
     4.3 @@ -59,16 +59,16 @@
     4.4    val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
     4.5  
     4.6    type tyco_syntax
     4.7 +  type simple_const_syntax
     4.8 +  type proto_const_syntax
     4.9    type const_syntax
    4.10 -  type proto_const_syntax
    4.11    val parse_infix: ('a -> 'b) -> lrx * int -> string
    4.12      -> int * ((fixity -> 'b -> Pretty.T)
    4.13      -> fixity -> 'a list -> Pretty.T)
    4.14    val parse_syntax: ('a -> 'b) -> OuterParse.token list
    4.15      -> (int * ((fixity -> 'b -> Pretty.T)
    4.16      -> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list
    4.17 -  val simple_const_syntax: (int * ((fixity -> iterm -> Pretty.T)
    4.18 -    -> fixity -> (iterm * itype) list -> Pretty.T)) option -> proto_const_syntax option
    4.19 +  val simple_const_syntax: simple_const_syntax -> proto_const_syntax
    4.20    val activate_const_syntax: theory -> literals
    4.21      -> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming
    4.22    val gen_print_app: (thm -> var_ctxt -> const * iterm list -> Pretty.T list)
    4.23 @@ -219,15 +219,17 @@
    4.24  
    4.25  type tyco_syntax = int * ((fixity -> itype -> Pretty.T)
    4.26    -> fixity -> itype list -> Pretty.T);
    4.27 -type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
    4.28 -  -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
    4.29 +
    4.30 +type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T)
    4.31 +  -> fixity -> (iterm * itype) list -> Pretty.T);
    4.32  type proto_const_syntax = int * (string list * (literals -> string list
    4.33    -> (var_ctxt -> fixity -> iterm -> Pretty.T)
    4.34      -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
    4.35 +type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
    4.36 +  -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
    4.37  
    4.38 -fun simple_const_syntax (SOME (n, f)) = SOME (n,
    4.39 -      ([], (fn _ => fn _ => fn print => fn thm => fn vars => f (print vars))))
    4.40 -  | simple_const_syntax NONE = NONE;
    4.41 +val simple_const_syntax =
    4.42 +  apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars))));
    4.43  
    4.44  fun activate_const_syntax thy literals (n, (cs, f)) naming =
    4.45    fold_map (Code_Thingol.ensure_declared_const thy) cs naming
    4.46 @@ -307,7 +309,7 @@
    4.47  
    4.48  fun parse_syntax prep_arg xs =
    4.49    Scan.option ((
    4.50 -      ((OuterParse.$$$ infixK  >> K X)
    4.51 +      ((OuterParse.$$$ infixK >> K X)
    4.52          || (OuterParse.$$$ infixlK >> K L)
    4.53          || (OuterParse.$$$ infixrK >> K R))
    4.54          -- OuterParse.nat >> parse_infix prep_arg
     5.1 --- a/src/Tools/Code/code_target.ML	Sat Dec 19 09:07:04 2009 -0800
     5.2 +++ b/src/Tools/Code/code_target.ML	Mon Dec 21 08:32:22 2009 +0100
     5.3 @@ -6,9 +6,8 @@
     5.4  
     5.5  signature CODE_TARGET =
     5.6  sig
     5.7 -  include CODE_PRINTER
     5.8 -
     5.9    type serializer
    5.10 +  type literals = Code_Printer.literals
    5.11    val add_target: string * (serializer * literals) -> theory -> theory
    5.12    val extend_target: string *
    5.13        (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
    5.14 @@ -39,6 +38,8 @@
    5.15    val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
    5.16  
    5.17    val allow_abort: string -> theory -> theory
    5.18 +  type tyco_syntax = Code_Printer.tyco_syntax
    5.19 +  type proto_const_syntax = Code_Printer.proto_const_syntax
    5.20    val add_syntax_class: string -> class -> string option -> theory -> theory
    5.21    val add_syntax_inst: string -> class * string -> unit option -> theory -> theory
    5.22    val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
    5.23 @@ -51,7 +52,11 @@
    5.24  struct
    5.25  
    5.26  open Basic_Code_Thingol;
    5.27 -open Code_Printer;
    5.28 +
    5.29 +type literals = Code_Printer.literals;
    5.30 +type tyco_syntax = Code_Printer.tyco_syntax;
    5.31 +type proto_const_syntax = Code_Printer.proto_const_syntax;
    5.32 +
    5.33  
    5.34  (** basics **)
    5.35  
    5.36 @@ -78,8 +83,8 @@
    5.37  datatype name_syntax_table = NameSyntaxTable of {
    5.38    class: string Symtab.table,
    5.39    instance: unit Symreltab.table,
    5.40 -  tyco: tyco_syntax Symtab.table,
    5.41 -  const: proto_const_syntax Symtab.table
    5.42 +  tyco: Code_Printer.tyco_syntax Symtab.table,
    5.43 +  const: Code_Printer.proto_const_syntax Symtab.table
    5.44  };
    5.45  
    5.46  fun mk_name_syntax_table ((class, instance), (tyco, const)) =
    5.47 @@ -103,14 +108,14 @@
    5.48    -> (string * Pretty.T) list           (*includes*)
    5.49    -> (string -> string option)          (*module aliasses*)
    5.50    -> (string -> string option)          (*class syntax*)
    5.51 -  -> (string -> tyco_syntax option)
    5.52 -  -> (string -> const_syntax option)
    5.53 +  -> (string -> Code_Printer.tyco_syntax option)
    5.54 +  -> (string -> Code_Printer.const_syntax option)
    5.55    -> ((Pretty.T -> string) * (Pretty.T -> unit))
    5.56    -> Code_Thingol.program
    5.57    -> string list                        (*selected statements*)
    5.58    -> serialization;
    5.59  
    5.60 -datatype serializer_entry = Serializer of serializer * literals
    5.61 +datatype serializer_entry = Serializer of serializer * Code_Printer.literals
    5.62    | Extends of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
    5.63  
    5.64  datatype target = Target of {
    5.65 @@ -273,7 +278,7 @@
    5.66      serializer module args (Code_Thingol.labelled_name thy program2) reserved includes
    5.67        (Symtab.lookup module_alias) (Symtab.lookup class')
    5.68        (Symtab.lookup tyco') (Symtab.lookup const')
    5.69 -      (string_of_pretty width, writeln_pretty width)
    5.70 +      (Code_Printer.string_of_pretty width, Code_Printer.writeln_pretty width)
    5.71        program4 names2
    5.72    end;
    5.73  
    5.74 @@ -396,32 +401,32 @@
    5.75  fun read_inst thy (raw_tyco, raw_class) =
    5.76    (read_class thy raw_class, read_tyco thy raw_tyco);
    5.77  
    5.78 -fun gen_add_syntax upd del mapp check_x get_check_syn prep target raw_x some_syn thy =
    5.79 +fun gen_add_syntax upd del mapp check_x check_raw_syn prep_syn prep_x target raw_x some_raw_syn thy =
    5.80    let
    5.81 -    val x = prep thy raw_x;
    5.82 -    fun check_syn thy syn = ();
    5.83 -  in case some_syn
    5.84 -   of SOME syn => (map_name_syntax target o mapp) (upd (x, (check_x thy x; check_syn thy syn; syn))) thy
    5.85 +    val x = prep_x thy raw_x |> tap (check_x thy);
    5.86 +    fun prep_check raw_syn = prep_syn (raw_syn |> tap (check_raw_syn thy target));
    5.87 +  in case some_raw_syn
    5.88 +   of SOME raw_syn => (map_name_syntax target o mapp) (upd (x, prep_check raw_syn)) thy
    5.89      | NONE => (map_name_syntax target o mapp) (del x) thy
    5.90    end;
    5.91  
    5.92 -fun gen_add_syntax_class prep =
    5.93 -  gen_add_syntax Symtab.update Symtab.delete_safe (apfst o apfst) (K I) I prep;
    5.94 +fun gen_add_syntax_class prep_class =
    5.95 +  gen_add_syntax Symtab.update Symtab.delete_safe (apfst o apfst) (K I) ((K o K o K) ()) I prep_class;
    5.96  
    5.97 -fun gen_add_syntax_inst prep =
    5.98 -  gen_add_syntax Symreltab.update Symreltab.delete_safe (apfst o apsnd) (K I) I prep;
    5.99 +fun gen_add_syntax_inst prep_inst =
   5.100 +  gen_add_syntax Symreltab.update Symreltab.delete_safe (apfst o apsnd) (K I) ((K o K o K) ()) I prep_inst;
   5.101  
   5.102 -fun gen_add_syntax_tyco prep =
   5.103 +fun gen_add_syntax_tyco prep_tyco =
   5.104    gen_add_syntax Symtab.update Symtab.delete_safe (apsnd o apfst)
   5.105      (fn thy => fn tyco => fn (n, _) => if n <> Sign.arity_number thy tyco
   5.106        then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
   5.107 -      else ()) I prep;
   5.108 +      else ()) ((K o K o K) ()) I prep_tyco;
   5.109  
   5.110 -fun gen_add_syntax_const prep =
   5.111 +fun gen_add_syntax_const prep_const check_raw_syn prep_syn =
   5.112    gen_add_syntax Symtab.update Symtab.delete_safe (apsnd o apsnd)
   5.113      (fn thy => fn c => fn (n, _) => if n > Code.args_number thy c
   5.114        then error ("Too many arguments in syntax for constant " ^ quote c)
   5.115 -      else ()) I prep;
   5.116 +      else ()) check_raw_syn prep_syn prep_const;
   5.117  
   5.118  fun add_reserved target =
   5.119    let
   5.120 @@ -438,7 +443,7 @@
   5.121                then warning ("Overwriting existing include " ^ name)
   5.122                else ();
   5.123              val cs = map (read_const thy) raw_cs;
   5.124 -          in Symtab.update (name, (str content, cs)) incls end
   5.125 +          in Symtab.update (name, (Code_Printer.str content, cs)) incls end
   5.126        | add (name, NONE) incls = Symtab.delete name incls;
   5.127    in map_includes target (add args) thy end;
   5.128  
   5.129 @@ -460,12 +465,6 @@
   5.130      val c = prep_const thy raw_c;
   5.131    in thy |> (CodeTargetData.map o apfst o apsnd) (insert (op =) c) end;
   5.132  
   5.133 -fun zip_list (x::xs) f g =
   5.134 -  f
   5.135 -  #-> (fn y =>
   5.136 -    fold_map (fn x => g |-- f >> pair x) xs
   5.137 -    #-> (fn xys => pair ((x, y) :: xys)));
   5.138 -
   5.139  
   5.140  (* concrete syntax *)
   5.141  
   5.142 @@ -474,6 +473,12 @@
   5.143  structure P = OuterParse
   5.144  and K = OuterKeyword
   5.145  
   5.146 +fun zip_list (x::xs) f g =
   5.147 +  f
   5.148 +  #-> (fn y =>
   5.149 +    fold_map (fn x => g |-- f >> pair x) xs
   5.150 +    #-> (fn xys => pair ((x, y) :: xys)));
   5.151 +
   5.152  fun parse_multi_syntax parse_thing parse_syntax =
   5.153    P.and_list1 parse_thing
   5.154    #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
   5.155 @@ -484,7 +489,8 @@
   5.156  val add_syntax_class = gen_add_syntax_class cert_class;
   5.157  val add_syntax_inst = gen_add_syntax_inst cert_inst;
   5.158  val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
   5.159 -val add_syntax_const = gen_add_syntax_const (K I);
   5.160 +val add_syntax_const_simple = gen_add_syntax_const (K I) ((K o K o K) ()) Code_Printer.simple_const_syntax;
   5.161 +val add_syntax_const = gen_add_syntax_const (K I) ((K o K o K) ()) I;
   5.162  val allow_abort = gen_allow_abort (K I);
   5.163  val add_reserved = add_reserved;
   5.164  val add_include = add_include;
   5.165 @@ -492,7 +498,9 @@
   5.166  val add_syntax_class_cmd = gen_add_syntax_class read_class;
   5.167  val add_syntax_inst_cmd = gen_add_syntax_inst read_inst;
   5.168  val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
   5.169 -val add_syntax_const_cmd = gen_add_syntax_const Code.read_const;
   5.170 +val add_syntax_const_simple_cmd = gen_add_syntax_const Code.read_const ((K o K o K) ()) Code_Printer.simple_const_syntax;
   5.171 +val add_syntax_const_cmd = gen_add_syntax_const Code.read_const ((K o K o K) ()) I;
   5.172 +
   5.173  val allow_abort_cmd = gen_allow_abort Code.read_const;
   5.174  
   5.175  fun parse_args f args =
   5.176 @@ -524,25 +532,23 @@
   5.177  
   5.178  val _ =
   5.179    OuterSyntax.command "code_instance" "define code syntax for instance" K.thy_decl (
   5.180 -    parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
   5.181 -      (Scan.option (P.minus >> K ()))
   5.182 +    parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname) (Scan.option (P.minus >> K ()))
   5.183      >> (Toplevel.theory oo fold) (fn (target, syns) =>
   5.184            fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
   5.185    );
   5.186  
   5.187  val _ =
   5.188    OuterSyntax.command "code_type" "define code syntax for type constructor" K.thy_decl (
   5.189 -    parse_multi_syntax P.xname (parse_syntax I)
   5.190 +    parse_multi_syntax P.xname (Code_Printer.parse_syntax I)
   5.191      >> (Toplevel.theory oo fold) (fn (target, syns) =>
   5.192            fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
   5.193    );
   5.194  
   5.195  val _ =
   5.196    OuterSyntax.command "code_const" "define code syntax for constant" K.thy_decl (
   5.197 -    parse_multi_syntax P.term_group (parse_syntax fst)
   5.198 +    parse_multi_syntax P.term_group (Code_Printer.parse_syntax fst)
   5.199      >> (Toplevel.theory oo fold) (fn (target, syns) =>
   5.200 -      fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const
   5.201 -        (Code_Printer.simple_const_syntax syn)) syns)
   5.202 +      fold (fn (raw_const, syn) => add_syntax_const_simple_cmd target raw_const syn) syns)
   5.203    );
   5.204  
   5.205  val _ =