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