src/HOL/ex/Term.ML

--- a/src/HOL/ex/Term.ML	Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/ex/Term.ML	Fri Mar 24 12:30:35 1995 +0100
@@ -119,7 +119,7 @@
 
 val [prem] = goal Term.thy
     "N: list(term(A)) ==>  \
-\    !M. <N,M>: pred_sexp^+ --> \
+\    !M. (N,M): pred_sexp^+ --> \
 \        Abs_map (cut h (pred_sexp^+) M) N = \
 \        Abs_map h N";
 by (rtac (prem RS list.induct) 1);