1.1 --- a/test/Tools/isac/Test_Some.thy	Thu May 24 17:13:58 2012 +0200
     1.2 +++ b/test/Tools/isac/Test_Some.thy	Thu May 24 18:40:07 2012 +0200
     1.3 @@ -13,6 +13,7 @@
     1.4  ML {* (*================== --> test/../inform.sml*)
     1.5  "--------- UC errpat, fillpat ---------------------------"; (*--> test/../interface.sml*)
     1.6  "--------- build fun is_exactly_equal, .....----------------------"; (*--> test/../inform.sml*)
     1.7 +"--------- build fun is_exactly_equal, .....----------------------"; (*--> test/../inform.sml*)
     1.8  states := [];
     1.9  CalcTree
    1.10  [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"], 
    1.11 @@ -66,10 +67,13 @@
    1.12  
    1.13  *}
    1.14  ML {*
    1.15 -get_obj g_tac pt (lev_on p)
    1.16 +print_depth 999;
    1.17 +get_obj g_tac pt (lev_on p);
    1.18 +print_depth 999;
    1.19  *}
    1.20  ML {*
    1.21 -Rewrite_Inst
    1.22 +Rewrite_Inst';
    1.23 +("",""): thm';
    1.24  *}
    1.25  ML {*
    1.26  val Appl (rewtac as Rewrite' (_, _, _, _, _, _, (res, _))) =
    1.27 @@ -80,13 +84,52 @@
    1.28  thmID_of_derivation_name
    1.29  *}
    1.30  ML {*
    1.31 +Thm.get_name_hint;
    1.32 +Thm.derivation_name;
    1.33 +*}
    1.34 +ML {* (*================== already in code*)
    1.35 +fun thm'_of_thm thm =
    1.36 +  ((thyID_of_derivation_name o Thm.get_name_hint) thm,
    1.37 +   (thmID_of_derivation_name o Thm.get_name_hint) thm): thm'
    1.38 +fun generate_inconsistent_rew (subs_opt, thm') (f', asm) (is, ctxt) (pos as (p,_)) pt =
    1.39 +  let
    1.40 +    val f = get_curr_formula (pt, pos) (*already done in find_fillpatterns, too*)
    1.41 +    val (pt,c) = 
    1.42 +      case subs_opt of
    1.43 +        NONE => cappend_atomic pt p (is, insert_assumptions asm ctxt) f
    1.44 +          (Rewrite thm') (f', asm) Inconsistent
    1.45 +      | SOME subs => cappend_atomic pt p (is, insert_assumptions asm ctxt) f
    1.46 +          (Rewrite_Inst (subs, thm')) (f', asm) Inconsistent
    1.47 +    val pt = update_branch pt p TransitiveB
    1.48 +  in (pt, (p,Res)) end
    1.49 +*}
    1.50 +text {*
    1.51 +Rewrite_Inst' (theory', rew_ord', rls, bool, subst, thm', term, (res, term list))
    1.52 +*}
    1.53 +ML {*
    1.54 +fun requestFillformula cI (errpatID, fillpatID) =
    1.55 +  let
    1.56 +    val ((pt, _), _) = get_calc cI
    1.57 +		    val pos as (p, _) = get_pos cI 1
    1.58 +    val fillforms = find_fillpatterns (pt, pos) errpatID 
    1.59 +  in
    1.60 +    case filter ((curry op = fillpatID) o 
    1.61 +        (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms of
    1.62 +      (_, fillform, thm, sube_opt) :: _ =>
    1.63 +        let
    1.64 +          val (pt, pos') = generate_inconsistent_rew (sube_opt, thm'_of_thm thm)
    1.65 +            (fillform, []) (get_loc pt pos) (lev_on p, Und) pt
    1.66 +        in
    1.67 +          (upd_calc cI ((pt, pos'), []); (*upd_ipos cI 1 pos';*)
    1.68 +           autocalculateOK2xml cI pos pos' pos')
    1.69 +        end
    1.70 +    | _ => autocalculateERROR2xml cI "no fillpattern found"    
    1.71 +  end;    
    1.72 +
    1.73  *}
    1.74  ML {*
    1.75  *}
    1.76 -ML {*
    1.77 -*}
    1.78 -ML {* (*================== changed here, not in code*)
    1.79 -*}
    1.80 +
    1.81  ML {* (*==================*)
    1.82  
    1.83  *}