src/ZF/Tools/datatype_package.ML

--- a/src/ZF/Tools/datatype_package.ML	Tue Nov 18 18:25:10 2008 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Tue Nov 18 18:25:42 2008 +0100
@@ -291,7 +291,7 @@
       (Ind_Syntax.traceIt "next case equation = " thy1 (mk_case_eqn arg))
       (*Proves a single case equation.  Could use simp_tac, but it's slower!*)
       (fn _ => EVERY
-        [rewtac con_def,
+        [rewrite_goals_tac [con_def],
          rtac case_trans 1,
          REPEAT (resolve_tac [refl, split_trans, Su.case_inl RS trans, Su.case_inr RS trans] 1)]);