1.1 --- a/src/Tools/isac/Interpret/inform.sml	Thu May 17 12:43:04 2012 +0200
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Thu May 17 16:44:13 2012 +0200
     1.3 @@ -659,25 +659,25 @@
     1.4     compare iform with calc-tree.form at pos by equ_nrls and all subsequent pos;
     1.5     collect all the tacs applied by the way;
     1.6     if "no derivation found" then check_error_patterns.
     1.7 -   ALTERNATIVE to check_error_patterns within compare_step seems too expensive.*)
     1.8 +   ALTERNATIVE: check_error_patterns _within_ compare_step seems too expensive.*)
     1.9  fun inform (cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate') istr =
    1.10    case parse (assoc_thy "Isac") istr of
    1.11 -	  SOME ifo =>
    1.12 +	  SOME f_in =>
    1.13  	    let
    1.14 -	      val ifo = term_of ifo
    1.15 -	      val fo =
    1.16 +	      val f_in = term_of f_in
    1.17 +	      val f_succ = (* the formula from "step pos cs" in appendFormula*)
    1.18  	        case p_ of
    1.19  	          Frm => get_obj g_form pt p
    1.20  			    | Res => (fst o (get_obj g_result pt)) p
    1.21  			    | _ => #3 (get_obj g_origin pt p)
    1.22  			in
    1.23 -			  if fo = ifo
    1.24 +			  if f_succ = f_in
    1.25  			  then ("same-formula", cs) (* ctree not cut with replaceFormula *)
    1.26  			  else
    1.27 -			    case cas_input ifo of
    1.28 +			    case cas_input f_in of
    1.29  			      SOME (pt, _) => ("ok",([], [], (pt, (p, Met))))
    1.30  			    | NONE =>
    1.31 -			        let val msg_calcstate' = compare_step ([], [], (pt, lev_back pos)) ifo
    1.32 +			        let val msg_calcstate' = compare_step ([], [], (pt, lev_back' pos)) f_in
    1.33  			          (*last step re-calc in compare_step TODO before WN09*)
    1.34  			        in
    1.35  			          case msg_calcstate' of
    1.36 @@ -685,9 +685,10 @@
    1.37  (*GOON
    1.38  			               let
    1.39  			                 val pp = par_pblobj pt p
    1.40 -			                 val {errpats, nrls, ...} = get_met (get_obj g_metID pt pp)
    1.41 +			                 val {errpats, nrls, scr = Script prog, ...} = get_met (get_obj g_metID pt pp)
    1.42 +			                 val ScrState (env, _, _, _, _, _) = get_istate pt pos
    1.43  			               in
    1.44 -			                 case check_error_patterns (fo, ifo) ?subst? errpats nrls of
    1.45 +			                 case check_error_patterns (f_succ, f_in) (prog, env) (errpats, nrls) of
    1.46  			                   SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')
    1.47  			                 | NONE => msg_calcstate'
    1.48  			               end