tuned Nitpick and Refute examples, which are too slow on some testing machines

--- a/src/HOL/ex/Refute_Examples.thy	Thu Sep 04 11:20:59 2014 +0200
+++ b/src/HOL/ex/Refute_Examples.thy	Thu Sep 04 11:53:39 2014 +0200
@@ -1207,27 +1207,6 @@
 
 (*****************************************************************************)
 
-subsubsection {* Records *}
-
-(*TODO: make use of pair types, rather than typedef, for record types*)
-
-record ('a, 'b) point =
-  xpos :: 'a
-  ypos :: 'b
-
-lemma "(x::('a, 'b) point) = y"
-refute [expect = genuine]
-oops
-
-record ('a, 'b, 'c) extpoint = "('a, 'b) point" +
-  ext :: 'c
-
-lemma "(x::('a, 'b, 'c) extpoint) = y"
-refute [expect = genuine]
-oops
-
-(*****************************************************************************)
-
 subsubsection {* Examples involving special functions *}
 
 lemma "card x = 0"

--- a/src/HOL/ex/Sudoku.thy	Thu Sep 04 11:20:59 2014 +0200
+++ b/src/HOL/ex/Sudoku.thy	Thu Sep 04 11:53:39 2014 +0200
@@ -19,7 +19,7 @@
 
 no_notation Groups.one_class.one ("1")
 
-datatype digit = A ("1") | B ("2") | C ("3") | D ("4") | E ("5") | F ("6") | G ("7") | H ("8") | I ("9")
+datatype_new digit = A ("1") | B ("2") | C ("3") | D ("4") | E ("5") | F ("6") | G ("7") | H ("8") | I ("9")
 
 definition valid :: "digit => digit => digit => digit => digit => digit => digit => digit => digit => bool" where