--- a/src/ZF/ex/Term.ML Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/Term.ML Fri Oct 10 18:23:31 1997 +0200
@@ -105,7 +105,7 @@
val [rew,tslist] = goal Term.thy
"[| !!t. j(t)==term_rec(t,d); ts: list(A) |] ==> \
-\ j(Apply(a,ts)) = d(a, ts, map(%Z.j(Z), ts))";
+\ j(Apply(a,ts)) = d(a, ts, map(%Z. j(Z), ts))";
by (rewtac rew);
by (rtac (tslist RS term_rec) 1);
qed "def_term_rec";
@@ -177,13 +177,13 @@
(** theorems about term_map **)
-goal Term.thy "!!t A. t: term(A) ==> term_map(%u.u, t) = t";
+goal Term.thy "!!t A. t: term(A) ==> term_map(%u. u, t) = t";
by (etac term_induct_eqn 1);
by (asm_simp_tac (!simpset addsimps [map_ident]) 1);
qed "term_map_ident";
goal Term.thy
- "!!t A. t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u.f(g(u)), t)";
+ "!!t A. t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u. f(g(u)), t)";
by (etac term_induct_eqn 1);
by (asm_simp_tac (!simpset addsimps [map_compose]) 1);
qed "term_map_compose";