--- 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"
--- 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