--- a/src/HOL/Library/Multiset.thy Fri Mar 06 18:21:32 2015 +0100
+++ b/src/HOL/Library/Multiset.thy Fri Mar 06 20:08:45 2015 +0100
@@ -1917,9 +1917,9 @@
val mset_nonempty_tac =
rtac @{thm nonempty_plus} ORELSE' rtac @{thm nonempty_single}
- val regroup_munion_conv =
- Function_Lib.regroup_conv @{const_abbrev Mempty} @{const_name plus}
- (map (fn t => t RS eq_reflection) (@{thms ac_simps} @ @{thms empty_neutral}))
+ fun regroup_munion_conv ctxt =
+ Function_Lib.regroup_conv ctxt @{const_abbrev Mempty} @{const_name plus}
+ (map (fn t => t RS eq_reflection) (@{thms ac_simps} @ @{thms empty_neutral}))
fun unfold_pwleq_tac i =
(rtac @{thm pw_leq_step} i THEN (fn st => unfold_pwleq_tac (i + 1) st))