1.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy Mon Sep 02 15:17:34 2013 +0200
1.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy Mon Sep 02 16:16:08 2013 +0200
1.3 @@ -71,8 +71,7 @@
1.4 the internal representation of "a + b * 3". The '...' indicate that some
1.5 details are still hidden; further details are received this way:
1.6 *}
1.7 -ML {* print_depth 99;
1.8 - @{term "a + b * 9"}
1.9 +ML {* print_depth 99; @{term "a + b * 9"}; print_depth 5;
1.10 *}
1.11 text {* The internal representation is too comprehensive for several kinds of
1.12 inspection. Thus ISAC provides additional features, as we see below. First