1.1 --- a/src/Tools/isac/Interpret/inform.sml	Tue May 22 13:40:06 2012 +0200
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Thu May 24 17:13:58 2012 +0200
     1.3 @@ -655,7 +655,7 @@
     1.4     (prog, env) for retrieval of casual substitution for bdv in the pattern. *)
     1.5  fun check_error_patterns (res, inf) (prog, env) (errpats, rls) =
     1.6    let
     1.7 -    val subst = get_bdv_subst prog env
     1.8 +    val (_, subst) = get_bdv_subst prog env
     1.9      fun scan (_, [], _) = NONE
    1.10        | scan (errpatID, errpat :: errpats, _) =
    1.11            case check_err_patt (res, inf) (subst: subst) (errpatID, errpat) rls of
    1.12 @@ -713,14 +713,15 @@
    1.13  			end
    1.14      | NONE => ("syntax error in '" ^ istr ^ "'", e_calcstate');
    1.15  
    1.16 -(* fill-in patterns an forms *)
    1.17 -fun get_fillform subst form errpatID ((fillpatID, pat, erpaID): fillpat) =
    1.18 +(* fill-in patterns an forms.
    1.19 +  returns thm required by "fun in_fillform *)
    1.20 +fun get_fillform (subs_opt, subst) (thm, form) errpatID ((fillpatID, pat, erpaID): fillpat) =
    1.21    let
    1.22      val (form', _, _, rewritten) =
    1.23        rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) form;
    1.24    in (*the fillpat of the thm must be dedicated to errpatID*)
    1.25      if errpatID = erpaID andalso rewritten
    1.26 -    then SOME (fillpatID, HOLogic.mk_eq (form, form')) else NONE end;
    1.27 +    then SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt) else NONE end;
    1.28  
    1.29  fun get_fillpats subst form errpatID thm =
    1.30        let
    1.31 @@ -728,7 +729,7 @@
    1.32          val (part, thyID) = thy_containing_thm thmDeriv
    1.33          val theID = [part, thyID, "Theorems", thmID_of_derivation_name thmDeriv]
    1.34          val Hthm {fillpats, ...} = get_the theID
    1.35 -        val some = map (get_fillform subst form errpatID) fillpats
    1.36 +        val some = map (get_fillform subst (thm, form) errpatID) fillpats
    1.37        in some |> filter is_some |> map the end;
    1.38  
    1.39  fun find_fillpatterns (pt, pos as (p, _): pos') errpatID =