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 ctxt (pt, ([6], Res)); |
55 val (Form form, SOME tac, asm) = ME_Misc.pt_extract ctxt (pt, ([6], Res)); |
56 case (UnparseC.term_in_ctxt @{context} form, tac, UnparseC.asms_test @{context} asm) of |
56 case (UnparseC.term @{context} form, tac, UnparseC.asms_test @{context} 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 []; |
61 if map (UnparseC.term_in_ctxt @{context}) asm = [] |
61 if map (UnparseC.term @{context}) asm = [] |
62 then () else error "solve.sml: interSteps on norm_Rational 2, asms"; |
62 then () else error "solve.sml: interSteps on norm_Rational 2, asms"; |