merged

--- a/src/HOL/Library/Multiset.thy	Fri Aug 22 14:39:40 2014 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Aug 25 08:45:32 2014 +0200
@@ -530,6 +530,17 @@
   "Multiset.filter P (M #\<inter> N) = Multiset.filter P M #\<inter> Multiset.filter P N"
   by (rule multiset_eqI) simp
 
+lemma multiset_filter_subset[simp]: "Multiset.filter f M \<le> M"
+  unfolding less_eq_multiset.rep_eq by auto
+
+lemma multiset_filter_mono: assumes "A \<le> B"
+  shows "Multiset.filter f A \<le> Multiset.filter f B"
+proof -
+  from assms[unfolded mset_le_exists_conv]
+  obtain C where B: "B = A + C" by auto
+  show ?thesis unfolding B by auto
+qed
+
 syntax
   "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{# _ :# _./ _#})")
 syntax (xsymbol)
@@ -1325,6 +1336,17 @@
   "mcard (multiset_of xs) = length xs"
   by (induct xs) simp_all
 
+lemma mcard_mono: assumes "A \<le> B"
+  shows "mcard A \<le> mcard B"
+proof -
+  from assms[unfolded mset_le_exists_conv]
+  obtain C where B: "B = A + C" by auto
+  show ?thesis unfolding B by (induct C, auto)
+qed
+
+lemma mcard_filter_lesseq[simp]: "mcard (Multiset.filter f M) \<le> mcard M"
+  by (rule mcard_mono[OF multiset_filter_subset])
+
 
 subsection {* Alternative representations *}
 

--- a/src/Pure/Isar/method.ML	Fri Aug 22 14:39:40 2014 +0200
+++ b/src/Pure/Isar/method.ML	Mon Aug 25 08:45:32 2014 +0200
@@ -474,8 +474,8 @@
             | _ =>
                 let
                   val facts =
-                    Attrib.partial_evaluation ctxt
-                      [((Binding.empty, [Attrib.internal (K att)]), thms)];
+                    Attrib.partial_evaluation ctxt [((Binding.name "dummy", []), thms)]
+                    |> map (fn (_, bs) => ((Binding.empty, [Attrib.internal (K att)]), bs));
                   fun decl phi =
                     Context.mapping I init #>
                     Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd;

--- a/src/Pure/ML/ml_thms.ML	Fri Aug 22 14:39:40 2014 +0200
+++ b/src/Pure/ML/ml_thms.ML	Mon Aug 25 08:45:32 2014 +0200
@@ -37,7 +37,6 @@
 val cons_thms = Data.map o apsnd o cons;
 
 
-
 (* attribute source *)
 
 val _ = Theory.setup