src/HOL/ex/Records.thy

  Functions on @{text point} schemes work for @{text cpoints} as well.
 *}
 
 constdefs
   foo10 :: nat
-  "foo10 == getX (| x = 2, y = 0, colour = Blue |)"
+  "foo10 == getX (| x = # 2, y = 0, colour = Blue |)"
 
 
 subsubsection {* Non-coercive structural subtyping *}
 
 text {*

  Great!
 *}
 
 constdefs
   foo11 :: cpoint
-  "foo11 == setX (| x = 2, y = 0, colour = Blue |) 0"
+  "foo11 == setX (| x = # 2, y = 0, colour = Blue |) 0"
 
 
 subsection {* Other features *}
 
 text {* Field names contribute to record identity. *}

   x' :: nat
   y' :: nat
 
 text {*
  \noindent May not apply @{term getX} to 
- @{term [source] "(| x' = 2, y' = 0 |)"}.
+ @{term [source] "(| x' = # 2, y' = 0 |)"}.
 *}
 
 text {* \medskip Polymorphic records. *}
 
 record 'a point'' = point +