src/HOL/Library/Multiset.thy
changeset 59625 aacdce52b2fc
parent 59557 ebd8ecacfba6
child 59807 22bc39064290
     1.1 --- a/src/HOL/Library/Multiset.thy	Fri Mar 06 18:21:32 2015 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Fri Mar 06 20:08:45 2015 +0100
     1.3 @@ -1917,9 +1917,9 @@
     1.4    val mset_nonempty_tac =
     1.5        rtac @{thm nonempty_plus} ORELSE' rtac @{thm nonempty_single}
     1.6  
     1.7 -  val regroup_munion_conv =
     1.8 -      Function_Lib.regroup_conv @{const_abbrev Mempty} @{const_name plus}
     1.9 -        (map (fn t => t RS eq_reflection) (@{thms ac_simps} @ @{thms empty_neutral}))
    1.10 +  fun regroup_munion_conv ctxt =
    1.11 +    Function_Lib.regroup_conv ctxt @{const_abbrev Mempty} @{const_name plus}
    1.12 +      (map (fn t => t RS eq_reflection) (@{thms ac_simps} @ @{thms empty_neutral}))
    1.13  
    1.14    fun unfold_pwleq_tac i =
    1.15      (rtac @{thm pw_leq_step} i THEN (fn st => unfold_pwleq_tac (i + 1) st))