src/ZF/ex/BT.ML

--- a/src/ZF/ex/BT.ML	Thu Aug 06 10:50:44 1998 +0200
+++ b/src/ZF/ex/BT.ML	Thu Aug 06 12:24:04 1998 +0200
@@ -50,8 +50,7 @@
 by (Simp_tac 1);
 qed "bt_rec_Lf";
 
-Goal
-    "bt_rec(Br(a,l,r), c, h) = h(a, l, r, bt_rec(l,c,h), bt_rec(r,c,h))";
+Goal "bt_rec(Br(a,l,r), c, h) = h(a, l, r, bt_rec(l,c,h), bt_rec(r,c,h))";
 by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
 by (simp_tac (rank_ss addsimps (bt.case_eqns @ [rank_Br1, rank_Br2])) 1);
 qed "bt_rec_Br";