test/Tools/isac/Interpret/error-pattern.sml
changeset 59977 e635534c5f63
parent 59976 950922a768ca
child 59978 660ed21464d2
     1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml	Thu May 14 09:30:40 2020 +0200
     1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml	Thu May 14 13:33:47 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, _))): Chead.calcstate'), istr)
     1.8 +"~~~~~ fun Step_Solve.by_term , args:"; val (((*next_*)cs as (_, _, (pt, pos as (p, _))): Specification.calcstate'), 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*);