diff -r 27f3c10b0b50 -r 4cf66f21b764 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Record.thy	Mon Dec 07 10:38:04 2015 +0100
@@ -18,14 +18,14 @@
 text \<open>
   Records are isomorphic to compound tuple types. To implement
   efficient records, we make this isomorphism explicit. Consider the
-  record access/update simplification @{text "alpha (beta_update f
-  rec) = alpha rec"} for distinct fields alpha and beta of some record
-  rec with n fields. There are @{text "n ^ 2"} such theorems, which
+  record access/update simplification \<open>alpha (beta_update f
+  rec) = alpha rec\<close> for distinct fields alpha and beta of some record
+  rec with n fields. There are \<open>n ^ 2\<close> such theorems, which
   prohibits storage of all of them for large n. The rules can be
   proved on the fly by case decomposition and simplification in O(n)
   time. By creating O(n) isomorphic-tuple types while defining the
   record, however, we can prove the access/update simplification in
-  @{text "O(log(n)^2)"} time.
+  \<open>O(log(n)^2)\<close> time.
 
   The O(n) cost of case decomposition is not because O(n) steps are
   taken, but rather because the resulting rule must contain O(n) new
@@ -34,39 +34,36 @@
   access/update theorems.
 
   Record types are defined as isomorphic to tuple types. For instance,
-  a record type with fields @{text "'a"}, @{text "'b"}, @{text "'c"}
-  and @{text "'d"} might be introduced as isomorphic to @{text "'a \<times>
-  ('b \<times> ('c \<times> 'd))"}. If we balance the tuple tree to @{text "('a \<times>
-  'b) \<times> ('c \<times> 'd)"} then accessors can be defined by converting to the
+  a record type with fields \<open>'a\<close>, \<open>'b\<close>, \<open>'c\<close>
+  and \<open>'d\<close> might be introduced as isomorphic to \<open>'a \<times>
+  ('b \<times> ('c \<times> 'd))\<close>. If we balance the tuple tree to \<open>('a \<times>
+  'b) \<times> ('c \<times> 'd)\<close> then accessors can be defined by converting to the
   underlying type then using O(log(n)) fst or snd operations.
-  Updators can be defined similarly, if we introduce a @{text
-  "fst_update"} and @{text "snd_update"} function. Furthermore, we can
+  Updators can be defined similarly, if we introduce a \<open>fst_update\<close> and \<open>snd_update\<close> function. Furthermore, we can
   prove the access/update theorem in O(log(n)) steps by using simple
-  rewrites on fst, snd, @{text "fst_update"} and @{text "snd_update"}.
+  rewrites on fst, snd, \<open>fst_update\<close> and \<open>snd_update\<close>.
 
   The catch is that, although O(log(n)) steps were taken, the
   underlying type we converted to is a tuple tree of size
   O(n). Processing this term type wastes performance. We avoid this
   for large n by taking each subtree of size K and defining a new type
   isomorphic to that tuple subtree. A record can now be defined as
-  isomorphic to a tuple tree of these O(n/K) new types, or, if @{text
-  "n > K*K"}, we can repeat the process, until the record can be
+  isomorphic to a tuple tree of these O(n/K) new types, or, if \<open>n > K*K\<close>, we can repeat the process, until the record can be
   defined in terms of a tuple tree of complexity less than the
   constant K.
 
   If we prove the access/update theorem on this type with the
-  analogous steps to the tuple tree, we consume @{text "O(log(n)^2)"}
-  time as the intermediate terms are @{text "O(log(n))"} in size and
+  analogous steps to the tuple tree, we consume \<open>O(log(n)^2)\<close>
+  time as the intermediate terms are \<open>O(log(n))\<close> in size and
   the types needed have size bounded by K.  To enable this analogous
-  traversal, we define the functions seen below: @{text
-  "iso_tuple_fst"}, @{text "iso_tuple_snd"}, @{text "iso_tuple_fst_update"}
-  and @{text "iso_tuple_snd_update"}. These functions generalise tuple
+  traversal, we define the functions seen below: \<open>iso_tuple_fst\<close>, \<open>iso_tuple_snd\<close>, \<open>iso_tuple_fst_update\<close>
+  and \<open>iso_tuple_snd_update\<close>. These functions generalise tuple
   operations by taking a parameter that encapsulates a tuple
   isomorphism.  The rewrites needed on these functions now need an
   additional assumption which is that the isomorphism works.
 
   These rewrites are typically used in a structured way. They are here
-  presented as the introduction rule @{text "isomorphic_tuple.intros"}
+  presented as the introduction rule \<open>isomorphic_tuple.intros\<close>
   rather than as a rewrite rule set. The introduction form is an
   optimisation, as net matching can be performed at one term location
   for each step rather than the simplifier searching the term for