src/HOL/Tools/datatype_codegen.ML
changeset 20435 d2a30fed7596
parent 20426 9ffea7a8b31c
child 20439 1bf42b262a38
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Wed Aug 30 08:29:30 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Wed Aug 30 08:30:09 2006 +0200
     1.3 @@ -370,6 +370,7 @@
     1.4    in map mk_dist (sym_product cos) end;
     1.5  
     1.6  local
     1.7 +  val not_sym = thm "HOL.not_sym";
     1.8    val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
     1.9  in fun get_eq thy dtco =
    1.10    let
    1.11 @@ -396,6 +397,7 @@
    1.12      val distinct =
    1.13        mk_distinct cos
    1.14        |> map (fn t => Goal.prove_global thy [] [] t (K tac))
    1.15 +      |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
    1.16    in inject1 @ inject2 @ distinct end;
    1.17  end (*local*);
    1.18