50 getTactic 1 ([6,1], Frm) (*here get the tactic, and ...*); |
50 getTactic 1 ([6,1], Frm) (*here get the tactic, and ...*); |
51 interSteps 1 ([6,1], Res) (*... here get the intermediate steps above*); |
51 interSteps 1 ([6,1], Res) (*... here get the intermediate steps above*); |
52 |
52 |
53 getTactic 1 ([6,1,1], Frm); (*WN130909 <ERROR> syserror in getTactic </ERROR>*) |
53 getTactic 1 ([6,1,1], Frm); (*WN130909 <ERROR> syserror in getTactic </ERROR>*) |
54 val ((pt,_),_) = States.get_calc 1; Test_Tool.show_pt pt; |
54 val ((pt,_),_) = States.get_calc 1; Test_Tool.show_pt pt; |
55 val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([6], Res)); |
55 val (Form form, SOME tac, asm) = ME_Misc.pt_extract ctxt (pt, ([6], Res)); |
56 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of |
56 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of |
57 ("1 / 2", Check_Postcond ["rational", "simplification"], []) => () |
57 ("1 / 2", Check_Postcond ["rational", "simplification"], []) => () |
58 | _ => error "solve.sml: interSteps on norm_Rational 2"; |
58 | _ => error "solve.sml: interSteps on norm_Rational 2"; |
59 get_obj g_res pt []; |
59 get_obj g_res pt []; |
60 val (t, asm) = get_obj g_result pt []; |
60 val (t, asm) = get_obj g_result pt []; |