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