src/HOL/Induct/QuoNestedDataType.thy

--- a/src/HOL/Induct/QuoNestedDataType.thy	Wed Nov 23 22:26:13 2005 +0100
+++ b/src/HOL/Induct/QuoNestedDataType.thy	Thu Nov 24 00:00:20 2005 +0100
@@ -265,7 +265,7 @@
 
 lemma listset_Rep_Exp_Abs_Exp:
      "listset (map Rep_Exp (Abs_ExpList Us)) = listrel exprel `` {Us}";
-by (induct_tac Us, simp_all add: listrel_Cons Abs_ExpList_def)
+by (induct Us, simp_all add: listrel_Cons Abs_ExpList_def)
 
 lemma FnCall:
      "FnCall F (Abs_ExpList Us) = Abs_Exp (exprel``{FNCALL F Us})"
@@ -459,4 +459,3 @@
 qed
 
 end
-