1.1 --- a/src/Tools/isac/Interpret/inform.sml	Mon May 21 07:59:57 2012 +0200
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Mon May 21 16:56:01 2012 +0200
     1.3 @@ -694,7 +694,7 @@
     1.4  			          val pos_pred = lev_back' pos
     1.5  			          (* f_pred ---"step pos cs"---> f_succ in appendFormula *)
     1.6  			          val f_pred = get_pred_formula (pt, pos_pred)
     1.7 -			          val msg_calcstate' = compare_step ([], [], (pt, pos_pred)) f_in
     1.8 +			          val msg_calcstate' = compare_step ([], [], (pt, pos_pred)) f_in (*<<=====*)
     1.9  			          (*last step re-calc in compare_step TODO before WN09*)
    1.10  			        in
    1.11  			          case msg_calcstate' of
    1.12 @@ -713,6 +713,36 @@
    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 +  let
    1.19 +    val (form', _, _, rewritten) =
    1.20 +      rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) form;
    1.21 +  in (*the fillpat of the thm must be dedicated to errpatID*)
    1.22 +    if errpatID = erpaID andalso rewritten
    1.23 +    then SOME (fillpatID, term2str (HOLogic.mk_eq (form, form'))) else NONE end;
    1.24 +
    1.25 +fun get_fillpats subst form errpatID thm =
    1.26 +      let
    1.27 +        val thmDeriv = Thm.get_name_hint thm
    1.28 +        val (part, thyID) = thy_containing_thm thmDeriv
    1.29 +        val theID = [part, thyID, "Theorems", thmID_of_derivation_name thmDeriv]
    1.30 +        val Hthm {fillpats, ...} = get_the theID
    1.31 +        val some = map (get_fillform subst form errpatID) fillpats
    1.32 +      in some |> filter is_some |> map the end;
    1.33 +
    1.34 +fun find_fillpatterns (pt, pos as (p, _): pos') errpatID =
    1.35 +  let 
    1.36 +    val f_curr = get_pred_formula (pt, pos); (* = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"*)
    1.37 +    val pp = par_pblobj pt p
    1.38 +			    val {errpats, scr = Script prog, ...} = get_met (get_obj g_metID pt pp)
    1.39 +    val ScrState (env, _, _, _, _, _) = get_istate pt pos
    1.40 +    val subst = get_bdv_subst prog env
    1.41 +    val errpatthms = errpats
    1.42 +      |> filter ((curry op = errpatID) o (#1: errpat -> errpatID))
    1.43 +      |> map (#3: errpat -> thm list)
    1.44 +      |> flat
    1.45 +  in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end;
    1.46  
    1.47  (*------------------------------------------------------------------(**)
    1.48  end