test/Tools/isac/Interpret/error-pattern.sml
changeset 59981 dc34eff67648
parent 59980 2cb6de68b115
child 59982 56654afad89f
     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*);