src/HOL/Tools/datatype_codegen.ML

         val t = HOLogic.mk_not prem;
       in HOLogic.mk_Trueprop t end;
   in map mk_dist (sym_product cos) end;
 
 local
+  val not_sym = thm "HOL.not_sym";
   val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
 in fun get_eq thy dtco =
   let
     val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco;
     fun mk_triv_inject co =

     val tac = ALLGOALS (simp_tac simpset)
       THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]);
     val distinct =
       mk_distinct cos
       |> map (fn t => Goal.prove_global thy [] [] t (K tac))
+      |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
   in inject1 @ inject2 @ distinct end;
 end (*local*);
 
 fun datatype_tac thy dtco =
   let