diff -r 3567d0571932 -r 8feb2c4bef1a src/CCL/Fix.thy
--- a/src/CCL/Fix.thy	Fri Apr 23 23:33:48 2010 +0200
+++ b/src/CCL/Fix.thy	Fri Apr 23 23:35:43 2010 +0200
@@ -98,7 +98,7 @@
 
 (* All fixed points are lam-expressions *)
 
-lemma idgenfp_lam: "idgen(d) = d ==> d = lam x. ?f(x)"
+schematic_lemma idgenfp_lam: "idgen(d) = d ==> d = lam x. ?f(x)"
   apply (unfold idgen_def)
   apply (erule ssubst)
   apply (rule refl)
@@ -130,7 +130,7 @@
   apply simp
   done
 
-lemma po_eta_lemma: "idgen(d) = d ==> d = lam x. ?f(x)"
+schematic_lemma po_eta_lemma: "idgen(d) = d ==> d = lam x. ?f(x)"
   apply (unfold idgen_def)
   apply (erule sym)
   done