src/HOL/Tools/datatype_package.ML
changeset 17875 d81094515061
parent 17521 0f1c48de39f5
child 17956 369e2af8ee45
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Oct 17 19:19:29 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Oct 17 23:10:10 2005 +0200
     1.3 @@ -352,7 +352,7 @@
     1.4                                      atac 2, resolve_tac thms 1, etac FalseE 1])))
     1.5                                 | ManyConstrs (thm, simpset) => SOME (Tactic.prove sg [] [] eq_t (K
     1.6                                     (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
     1.7 -                                    full_simp_tac (Simplifier.inherit_bounds ss simpset) 1,
     1.8 +                                    full_simp_tac (Simplifier.inherit_context ss simpset) 1,
     1.9                                      REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
    1.10                                      eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1,
    1.11                                      etac FalseE 1]))))
    1.12 @@ -372,7 +372,7 @@
    1.13  
    1.14  val simproc_setup =
    1.15    [Theory.add_oracle (distinctN, fn (_, ConstrDistinct t) => t),
    1.16 -   fn thy => (simpset_ref_of thy := simpset_of thy addsimprocs [distinct_simproc]; thy)];
    1.17 +   fn thy => ((change_simpset_of thy) (fn ss => ss addsimprocs [distinct_simproc]); thy)];
    1.18  
    1.19  
    1.20  (**** translation rules for case ****)