src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Tue Apr 12 13:49:37 2016 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Tue Apr 12 14:38:57 2016 +0200
@@ -120,7 +120,7 @@
       th RS @{thm eq_reflection}
   | _ => th)
 
-val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
+val meta_fun_cong = @{lemma "\<And>f :: 'a::{} \<Rightarrow> 'b::{}.f == g ==> f x == g x" by simp}
 
 fun full_fun_cong_expand th =
   let