# HG changeset patch
# User blanchet
# Date 1409652812 -7200
# Node ID 3bfd12e456f42decd7ce12703c6e74e3339f9295
# Parent  feb69891e0fdabfb6c1ae9f128945303a407991c# Parent  0774d32fe74f4623b17f6e23ad7d3538984269b2
merge

diff -r 0774d32fe74f -r 3bfd12e456f4 src/HOL/BNF_Least_Fixpoint.thy
--- a/src/HOL/BNF_Least_Fixpoint.thy	Tue Sep 02 09:28:23 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy	Tue Sep 02 12:13:32 2014 +0200
@@ -155,16 +155,12 @@
 lemma insert_subsetI: "\<lbrakk>x \<in> A; X \<subseteq> A\<rbrakk> \<Longrightarrow> insert x X \<subseteq> A"
 by auto
 
-(*helps resolution*)
-lemma well_order_induct_imp:
-  "wo_rel r \<Longrightarrow> (\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> y \<in> Field r \<longrightarrow> P y \<Longrightarrow> x \<in> Field r \<longrightarrow> P x) \<Longrightarrow>
-     x \<in> Field r \<longrightarrow> P x"
-by (erule wo_rel.well_order_induct)
+lemmas well_order_induct_imp = wo_rel.well_order_induct[of r "\<lambda>x. x \<in> Field r \<longrightarrow> P x" for r P]
 
 lemma meta_spec2:
   assumes "(\<And>x y. PROP P x y)"
   shows "PROP P x y"
-by (rule assms)
+  by (rule assms)
 
 lemma nchotomy_relcomppE:
   assumes "\<And>y. \<exists>x. y = f x" "(r OO s) a c" "\<And>b. r a (f b) \<Longrightarrow> s (f b) c \<Longrightarrow> P"
diff -r 0774d32fe74f -r 3bfd12e456f4 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Tue Sep 02 09:28:23 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Tue Sep 02 12:13:32 2014 +0200
@@ -263,7 +263,7 @@
   else
     thy;
 
-fun new_interpretation_of nesting_pref f fp_sugars thy =
+fun new_interpretation_of nesting_pref f (fp_sugars : fp_sugar list) thy =
   let val T_names = map (fst o dest_Type o #T) fp_sugars in
     if nesting_pref = Keep_Nesting orelse
         exists (is_none o Old_Datatype_Data.get_info thy) T_names then