1.1 --- a/src/Tools/isac/Interpret/inform.sml	Wed May 16 15:47:22 2012 +0200
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Thu May 17 12:43:04 2012 +0200
     1.3 @@ -632,18 +632,18 @@
     1.4    end;
     1.5  
     1.6  (* check if (agreed result, input formula) matches an error pattern modulo simplifier rls*)
     1.7 -fun check_err_patt (res, inf) (errpatID: errpatID, pat) rls =
     1.8 +fun check_err_patt (res, inf) (subst: subst) (errpatID: errpatID, pat) rls =
     1.9    let 
    1.10      val (res', _, _, rewritten) =
    1.11 -      rew_sub (Isac()) 1 [] e_rew_ord e_rls false [] (Trueprop $ pat) res;
    1.12 +      rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) res;
    1.13    in
    1.14      if rewritten
    1.15      then 
    1.16        let
    1.17 -        val norm_res = case rewrite_set_ (Isac()) false rls res' of
    1.18 +        val norm_res = case rewrite_set_inst_ (Isac()) false subst rls  res' of
    1.19            NONE => res'
    1.20          | SOME (norm_res, _) => norm_res
    1.21 -        val norm_inf = case rewrite_set_ (Isac()) false rls inf of
    1.22 +        val norm_inf = case rewrite_set_inst_ (Isac()) false subst rls inf of
    1.23            NONE => inf
    1.24          | SOME (norm_inf, _) => norm_inf
    1.25        in if norm_res = norm_inf then SOME errpatID else NONE
    1.26 @@ -658,7 +658,8 @@
    1.27  formula, which is no CAS-command:
    1.28     compare iform with calc-tree.form at pos by equ_nrls and all subsequent pos;
    1.29     collect all the tacs applied by the way;
    1.30 -   if "no derivation found" then check_error_patterns.*)
    1.31 +   if "no derivation found" then check_error_patterns.
    1.32 +   ALTERNATIVE to check_error_patterns within compare_step seems too expensive.*)
    1.33  fun inform (cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate') istr =
    1.34    case parse (assoc_thy "Isac") istr of
    1.35  	  SOME ifo =>
    1.36 @@ -677,14 +678,25 @@
    1.37  			      SOME (pt, _) => ("ok",([], [], (pt, (p, Met))))
    1.38  			    | NONE =>
    1.39  			        let val msg_calcstate' = compare_step ([], [], (pt, lev_back pos)) ifo
    1.40 -			        (*last step re-calc in compare_step TODO before WN09*)
    1.41 +			          (*last step re-calc in compare_step TODO before WN09*)
    1.42  			        in
    1.43  			          case msg_calcstate' of
    1.44 -			            ("no derivation found", _) => msg_calcstate' (*GOON*)
    1.45 +			            ("no derivation found", calcstate') => 
    1.46 +(*GOON
    1.47 +			               let
    1.48 +			                 val pp = par_pblobj pt p
    1.49 +			                 val {errpats, nrls, ...} = get_met (get_obj g_metID pt pp)
    1.50 +			               in
    1.51 +			                 case check_error_patterns (fo, ifo) ?subst? errpats nrls of
    1.52 +			                   SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')
    1.53 +			                 | NONE => msg_calcstate'
    1.54 +			               end
    1.55 +GOON*)
    1.56 +                       msg_calcstate'
    1.57  			          | _ => msg_calcstate'
    1.58  			        end
    1.59  			end
    1.60 -    | NONE => ("syntax error in '"^istr^"'", e_calcstate');
    1.61 +    | NONE => ("syntax error in '" ^ istr ^ "'", e_calcstate');
    1.62  
    1.63  
    1.64  (*------------------------------------------------------------------(**)