src/HOL/Univ.ML
changeset 8114 09a7a180cc99
parent 7255 853bdbe9973d
child 8292 93e125b21220
--- a/src/HOL/Univ.ML	Fri Jan 07 11:04:15 2000 +0100
+++ b/src/HOL/Univ.ML	Fri Jan 07 11:06:03 2000 +0100
@@ -206,7 +206,7 @@
 AddIffs  [Scons_not_Atom, Atom_not_Scons, Scons_Scons_eq];
 
 
-Goalw [ndepth_def] "ndepth (Abs_Node((%k. Inr 0, x))) = 0";
+Goalw [ndepth_def] "ndepth (Abs_Node(%k. Inr 0, x)) = 0";
 by (EVERY1[stac (Node_K0_I RS Abs_Node_inverse), stac split]);
 by (rtac Least_equality 1);
 by (rtac refl 1);