--- 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