src/HOL/Tools/datatype_package.ML
changeset 13480 bb72bd43c6c3
parent 13466 42766aa25460
child 13641 63d1790a43ed
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Aug 08 23:42:49 2002 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Aug 08 23:46:09 2002 +0200
     1.3 @@ -349,15 +349,15 @@
     1.4                               in (case (#distinct (datatype_info_sg_err sg tname1)) of
     1.5                                   QuickAndDirty => Some (Thm.invoke_oracle
     1.6                                     Datatype_thy distinctN (sg, ConstrDistinct eq_t))
     1.7 -                               | FewConstrs thms => Some (prove_goalw_cterm [] eq_ct (K
     1.8 -                                   [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, ss) => Some (prove_goalw_cterm [] eq_ct (K
    1.11 -                                   [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
    1.12 +                               | FewConstrs thms => Some (Tactic.prove sg [] [] eq_t (K
    1.13 +                                   (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
    1.14 +                                    atac 2, resolve_tac thms 1, etac FalseE 1])))
    1.15 +                               | ManyConstrs (thm, ss) => Some (Tactic.prove sg [] [] eq_t (K
    1.16 +                                   (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
    1.17                                      full_simp_tac ss 1,
    1.18                                      REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
    1.19                                      eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1,
    1.20 -                                    etac FalseE 1])))
    1.21 +                                    etac FalseE 1]))))
    1.22                               end
    1.23                             else None
    1.24                          end