diff -r aa6c470a962a -r 560372b461e5 src/HOL/Tools/Predicate_Compile/pred_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Sat Oct 24 16:54:32 2009 +0200
@@ -81,11 +81,13 @@
     Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _) => th RS @{thm eq_reflection}
   | _ => th
 
+val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
+
 fun full_fun_cong_expand th =
   let
     val (f, args) = strip_comb (fst (Logic.dest_equals (prop_of th)))
     val i = length (binder_types (fastype_of f)) - length args
-  in funpow i (fn th => th RS @{thm meta_fun_cong}) th end;
+  in funpow i (fn th => th RS meta_fun_cong) th end;
 
 fun declare_names s xs ctxt =
   let