# HG changeset patch
# User bulwahn
# Date 1256396072 -7200
# Node ID 560372b461e59a1580142f4b87ee5f39f8820b06
# Parent  aa6c470a962a95c83dd6c9ca6191d95d3c681a11
moved meta_fun_cong lemma into ML-file; tuned

diff -r aa6c470a962a -r 560372b461e5 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/Predicate.thy	Sat Oct 24 16:54:32 2009 +0200
@@ -770,10 +770,6 @@
    (auto simp add: Seq_def the_only_singleton is_empty_def
       null_is_empty singleton_bot singleton_single singleton_sup Let_def)
 
-lemma meta_fun_cong:
-"f == g ==> f x == g x"
-by simp
-
 ML {*
 signature PREDICATE =
 sig
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
diff -r aa6c470a962a -r 560372b461e5 src/HOL/ex/Predicate_Compile_ex.thy
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Sat Oct 24 16:54:32 2009 +0200
@@ -361,8 +361,8 @@
 (*quickcheck[generator = pred_compile, size=5, iterations=1]*)
 oops
 
+section {* Lambda *}
 
-section {* Lambda *}
 datatype type =
     Atom nat
   | Fun type type    (infixr "\<Rightarrow>" 200)