equal
deleted
inserted
replaced
369 end |
369 end |
370 |
370 |
371 (* compare inform with ctree.form at current pos by nrls; |
371 (* compare inform with ctree.form at current pos by nrls; |
372 if found, embed the derivation generated during comparison |
372 if found, embed the derivation generated during comparison |
373 if not, let the mat-engine compute the next ctree.form *) |
373 if not, let the mat-engine compute the next ctree.form *) |
374 (* structure copied from complete_solve |
374 (* code's structure is copied from complete_solve |
375 CAUTION: tacis in returned calcstate' do NOT construct resulting ptp -- |
375 CAUTION: tacis in returned calcstate' do NOT construct resulting ptp -- |
376 all_modspec etc. has to be inserted at Subproblem'*) |
376 all_modspec etc. has to be inserted at Subproblem'*) |
377 fun compare_step ((tacis, c, ptp as (pt, pos as (p,p_))): Chead.calcstate') ifo = |
377 fun compare_step ((tacis, c, ptp as (pt, pos as (p,p_))): Chead.calcstate') ifo = |
378 let |
378 let |
379 val fo = |
379 val fo = |