src/HOL/Tools/Datatype/datatype_codegen.ML
changeset 35899 e810f73c8ee2
parent 35845 e5980f0ad025
child 36298 2d55c4aba1dc
equal deleted inserted replaced
35898:c890a3835d15 35899:e810f73c8ee2
   356     val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr] vs) index);
   356     val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr] vs) index);
   357     fun prep_distinct (trueprop $ (not $ (_ $ t1 $ t2))) =
   357     fun prep_distinct (trueprop $ (not $ (_ $ t1 $ t2))) =
   358       [trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)];
   358       [trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)];
   359     val distincts = maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr] vs) index));
   359     val distincts = maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr] vs) index));
   360     val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
   360     val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
   361     val simpset = Simplifier.context (ProofContext.init thy) (HOL_basic_ss addsimps 
   361     val simpset = Simplifier.global_context thy (HOL_basic_ss addsimps 
   362       (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
   362       (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
   363     fun prove prop = Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
   363     fun prove prop = Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
   364       |> Simpdata.mk_eq;
   364       |> Simpdata.mk_eq;
   365   in (map prove (triv_injects @ injects @ distincts), prove refl) end;
   365   in (map prove (triv_injects @ injects @ distincts), prove refl) end;
   366 
   366