1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Thu May 14 15:06:18 2020 +0200
1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Thu May 14 16:08:41 2020 +0200
1.3 @@ -1022,7 +1022,7 @@
1.4 (*+*)if pos = ([1], Res) then () else error "inform with (positive) Error_Pattern.check_for broken 1";
1.5 val ("ok", cs' as (_, _, ptp)) = (*case*) Step.do_next pos cs (*of*);
1.6 (*case*) Step_Solve.by_term ptp (encode ifo) (*of*); (*ERROR WAS: "no derivation found"*)
1.7 -"~~~~~ fun Step_Solve.by_term , args:"; val (((*next_*)cs as (_, _, (pt, pos as (p, _))): Specification.calcstate'), istr)
1.8 +"~~~~~ fun Step_Solve.by_term , args:"; val (((*next_*)cs as (_, _, (pt, pos as (p, _))): Calc.state_post), istr)
1.9 = (cs', (encode ifo));
1.10 val ctxt = get_ctxt pt pos (*see TODO.thy*)
1.11 val SOME f_in = (*case*) TermC.parse (ThyC.get_theory "Isac_Knowledge") istr (*of*);