diff -r bb18eed53ed6 -r a1119cf551e8 src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Tue Aug 13 14:20:22 2013 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Tue Aug 13 16:25:47 2013 +0200
@@ -447,11 +447,11 @@
 begin
 
 definition
-  "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^isub>1)"
+  "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^sub>1)"
 
 definition enum_term_of_finite_1 :: "Enum.finite_1 itself => unit => term list"
 where
-  "enum_term_of_finite_1 = (%_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^isub>1])"
+  "enum_term_of_finite_1 = (%_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^sub>1])"
 
 instance ..
 
@@ -461,8 +461,8 @@
 begin
 
 definition
-  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>1)
-    orelse f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>2))"
+  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>1)
+    orelse f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>2))"
 
 definition enum_term_of_finite_2 :: "Enum.finite_2 itself => unit => term list"
 where
@@ -476,9 +476,9 @@
 begin
 
 definition
-  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>1)
-    orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>2)
-    orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>3))"
+  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>1)
+    orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>2)
+    orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>3))"
 
 definition enum_term_of_finite_3 :: "Enum.finite_3 itself => unit => term list"
 where
@@ -492,10 +492,10 @@
 begin
 
 definition
-  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>1)
-    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>2)
-    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>3)
-    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>4))"
+  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>1)
+    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>2)
+    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>3)
+    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>4))"
 
 definition enum_term_of_finite_4 :: "Enum.finite_4 itself => unit => term list"
 where