src/HOL/Tools/datatype_package.ML
changeset 16973 b2a894562b8f
parent 16672 f83f3aef274d
child 17057 0934ac31985f
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Aug 01 19:20:25 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Aug 01 19:20:26 2005 +0200
     1.3 @@ -326,7 +326,7 @@
     1.4  
     1.5  exception ConstrDistinct of term;
     1.6  
     1.7 -fun distinct_proc sg _ (t as Const ("op =", _) $ t1 $ t2) =
     1.8 +fun distinct_proc sg ss (t as Const ("op =", _) $ t1 $ t2) =
     1.9    (case (stripC (0, t1), stripC (0, t2)) of
    1.10       ((i, Const (cname1, T1)), (j, Const (cname2, T2))) =>
    1.11           (case (stripT (0, T1), stripT (0, T2)) of
    1.12 @@ -347,9 +347,9 @@
    1.13                                 | FewConstrs thms => SOME (Tactic.prove sg [] [] eq_t (K
    1.14                                     (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
    1.15                                      atac 2, resolve_tac thms 1, etac FalseE 1])))
    1.16 -                               | ManyConstrs (thm, ss) => SOME (Tactic.prove sg [] [] eq_t (K
    1.17 +                               | ManyConstrs (thm, simpset) => SOME (Tactic.prove sg [] [] eq_t (K
    1.18                                     (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
    1.19 -                                    full_simp_tac ss 1,
    1.20 +                                    full_simp_tac (Simplifier.inherit_bounds ss simpset) 1,
    1.21                                      REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
    1.22                                      eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1,
    1.23                                      etac FalseE 1]))))