# HG changeset patch
# User traytel
# Date 1365692334 -7200
# Node ID 1ce319118d59ed36a0f764cd2c97fa1c660125f5
# Parent  745a074246c283271836071aba96e81ae889a8ad
do not add case translation syntax in rep_datatype compatibility mode

diff -r 745a074246c2 -r 1ce319118d59 src/HOL/BNF/Tools/bnf_wrap.ML
--- a/src/HOL/BNF/Tools/bnf_wrap.ML	Thu Apr 11 16:39:01 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Thu Apr 11 16:58:54 2013 +0200
@@ -640,9 +640,10 @@
         ((discs, selss, exhaust_thm, inject_thms, distinct_thms, case_thms, disc_thmss, discI_thms,
           sel_thmss),
           lthy
-          |> Local_Theory.declaration {syntax = false, pervasive = true}
-             (fn phi => Case_Translation.register
-               (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
+          |> not rep_compat ?
+             (Local_Theory.declaration {syntax = false, pervasive = true}
+               (fn phi => Case_Translation.register
+                 (Morphism.term phi casex) (map (Morphism.term phi) ctrs)))
           |> Local_Theory.notes (notes' @ notes) |> snd)
       end;
   in