src/HOL/Tools/BNF/bnf_gfp.ML

--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Fri Feb 21 00:09:56 2014 +0100
@@ -1129,7 +1129,7 @@
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
     val strT_defs = map (fn def =>
-        trans OF [Morphism.thm phi def RS meta_eq_to_obj_eq RS fun_cong, @{thm prod.cases}])
+        trans OF [Morphism.thm phi def RS meta_eq_to_obj_eq RS fun_cong, @{thm prod.case}])
       strT_def_frees;
     val strTs = map (fst o Term.dest_Const o Morphism.term phi) strT_frees;