1.1 --- a/src/Tools/isac/calcelems.sml Tue Sep 14 15:46:56 2010 +0200
1.2 +++ b/src/Tools/isac/calcelems.sml Thu Sep 23 08:43:36 2010 +0200
1.3 @@ -283,17 +283,17 @@
1.4 (see match_ags).
1.5
1.6 Preliminary solution:
1.7 - # the thy in 'SubProblem (thy_, pbl, arglist)' is not taken automatically,
1.8 - # instead the 'maxthy (rootthy pt) thy_' is taken for each subpbl
1.9 + # the thy in 'SubProblem (thy', pbl, arglist)' is not taken automatically,
1.10 + # instead the 'maxthy (rootthy pt) thy' is taken for each subpbl
1.11 # however, a thy specified by the user in the rootpbl may lead to
1.12 errors in far-off subpbls (which are not yet reported properly !!!)
1.13 and interactively specifiying thys in subpbl is not very relevant.
1.14
1.15 Other solutions possible:
1.16 - # always parse and type-check with Isac.thy
1.17 + # always parse and type-check with theory "Isac"
1.18 (rejected tue to the vague idea eg. to re-use equations for R in C etc.)
1.19 # regard the subthy-relation in specifying thys of subpbls
1.20 - # specifically handle 'SubProblem (undefined_, pbl, arglist)'
1.21 + # specifically handle 'SubProblem (undefined, pbl, arglist)'
1.22 # ???
1.23 .*)
1.24 (*WN0509 TODO "ProtoPure" ... would be more consistent