test/Tools/isac/MathEngBasic/ctree.sml
changeset 60733 4097c1317986
parent 60705 b719a0b7c6b5
     1.1 --- a/test/Tools/isac/MathEngBasic/ctree.sml	Thu Aug 17 08:01:45 2023 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/ctree.sml	Fri Aug 18 18:51:18 2023 +0200
     1.3 @@ -768,16 +768,6 @@
     1.4  fun tlp [] = [0]     | tlp [_] = [0]     | tlp x = tl x;
     1.5  fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;
     1.6  
     1.7 -(*see modspec.sml#pt_form
     1.8 -fun pt_form (PrfObj {form,...}) = UnparseC.term @{context} form
     1.9 -  | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
    1.10 -    let val (dI, pI, _) = get_somespec' spec spec'
    1.11 -	val {cas,...} = Problem.from_store pI
    1.12 -    in case cas of
    1.13 -	   NONE => UnparseC.term @{context} (pblterm dI pI)
    1.14 -	 | SOME t => UnparseC.term @{context} (subst_atomic (Pre_Conds.environment probl) t)
    1.15 -    end;
    1.16 -*)
    1.17  (*.get an 'interval' from ctree down to a certain level
    1.18     by 'take_fromto children' of the nodes with specific 'from' and 'to';
    1.19     'i > 0' suppresses output during recursive descent towards 'from'