src/HOL/Tools/datatype_package.ML
changeset 20054 24d176b8f240
parent 19925 3f9341831812
child 20071 8f3e1ddb50e6
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Sat Jul 08 12:54:41 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Sat Jul 08 12:54:42 2006 +0200
     1.3 @@ -364,15 +364,17 @@
     1.4                               in (case (#distinct (the_datatype thy tname1)) of
     1.5                                   QuickAndDirty => SOME (Thm.invoke_oracle
     1.6                                     Datatype_thy distinctN (thy, ConstrDistinct eq_t))
     1.7 -                               | FewConstrs thms => SOME (Goal.prove thy [] [] eq_t (K
     1.8 -                                   (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
     1.9 -                                    atac 2, resolve_tac thms 1, etac FalseE 1])))
    1.10 -                               | ManyConstrs (thm, simpset) => SOME (Goal.prove thy [] [] eq_t (K
    1.11 -                                   (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
    1.12 -                                    full_simp_tac (Simplifier.inherit_context ss simpset) 1,
    1.13 -                                    REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
    1.14 -                                    eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1,
    1.15 -                                    etac FalseE 1]))))
    1.16 +                               | FewConstrs thms =>
    1.17 +                                   SOME (Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
    1.18 +                                     (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
    1.19 +                                       atac 2, resolve_tac thms 1, etac FalseE 1])))
    1.20 +                               | ManyConstrs (thm, simpset) =>
    1.21 +                                   SOME (Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
    1.22 +                                     (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
    1.23 +                                      full_simp_tac (Simplifier.inherit_context ss simpset) 1,
    1.24 +                                      REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
    1.25 +                                      eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1,
    1.26 +                                      etac FalseE 1]))))
    1.27                               end
    1.28                             else NONE
    1.29                          end
    1.30 @@ -380,7 +382,7 @@
    1.31                  else NONE
    1.32            | _ => NONE)
    1.33     | _ => NONE)
    1.34 -  | distinct_proc thy _ _ = NONE;
    1.35 +  | distinct_proc _ _ _ = NONE;
    1.36  
    1.37  val distinct_simproc =
    1.38    Simplifier.simproc HOL.thy distinctN ["s = t"] distinct_proc;
    1.39 @@ -741,7 +743,8 @@
    1.40      val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms new_type_names descr
    1.41        sorts induct case_names_exhausts thy2;
    1.42      val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms
    1.43 -      flat_names new_type_names descr sorts dt_info inject dist_rewrites dist_ss induct thy3;
    1.44 +      flat_names new_type_names descr sorts dt_info inject dist_rewrites
    1.45 +      (Simplifier.theory_context thy3 dist_ss) induct thy3;
    1.46      val ((case_thms, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
    1.47        flat_names new_type_names descr sorts reccomb_names rec_thms thy4;
    1.48      val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms new_type_names
    1.49 @@ -840,7 +843,8 @@
    1.50        DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction
    1.51          case_names_exhausts;
    1.52      val ((reccomb_names, rec_thms), thy3) = DatatypeAbsProofs.prove_primrec_thms
    1.53 -      false new_type_names [descr] sorts dt_info inject distinct dist_ss induction thy2;
    1.54 +      false new_type_names [descr] sorts dt_info inject distinct
    1.55 +      (Simplifier.theory_context thy2 dist_ss) induction thy2;
    1.56      val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms false
    1.57        new_type_names [descr] sorts reccomb_names rec_thms thy3;
    1.58      val (split_thms, thy5) = DatatypeAbsProofs.prove_split_thms