1.1 --- a/test/Tools/isac/Interpret/generate.sml	Fri May 25 09:58:20 2012 +0200
     1.2 +++ b/test/Tools/isac/Interpret/generate.sml	Fri May 25 16:30:15 2012 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4  		    val pos as (p, _) = get_pos cI 1;
     1.5      val fillforms = find_fillpatterns (pt, pos) errpatID;
     1.6  
     1.7 -if pos = ([1], Res) then () else error "requestFillformula changed 1";
     1.8 +if pos = ([1], Res) then () else error "generate_inconsistent_rew changed 1";
     1.9  
    1.10   val (_, fillform, thm, sube_opt) :: _ = filter ((curry op = fillpatID) o 
    1.11          (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms;
    1.12 @@ -50,9 +50,9 @@
    1.13      val f = get_curr_formula (pt, pos);
    1.14      val pos' as (p', _) = (lev_on p, Res);
    1.15  
    1.16 -if pos = ([1], Res) then () else error "requestFillformula changed 2a";
    1.17 +if pos = ([1], Res) then () else error "generate_inconsistent_rew changed 2a";
    1.18  if term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
    1.19 -  then () else error "requestFillformula changed 2b";
    1.20 +  then () else error "generate_inconsistent_rew changed 2b";
    1.21  
    1.22      val (pt,c) = 
    1.23        case subs_opt of
    1.24 @@ -60,19 +60,24 @@
    1.25            (Rewrite thm') (f', []) Inconsistent
    1.26        | SOME subs => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f
    1.27            (Rewrite_Inst (subs, thm')) (f', []) Inconsistent
    1.28 -    val pt = update_branch pt p TransitiveB;
    1.29 +    val pt = update_branch pt p' TransitiveB;
    1.30 +
    1.31 +if get_obj g_tac pt p' = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", ""))
    1.32 +  andalso pos = ([1], Res) andalso pos' = ([2], Res) andalso p' = [2]
    1.33 +then () else error "generate_inconsistent_rew changed 3";
    1.34  
    1.35  "~~~~~ to requestFillformula return val:"; val (pt, pos') = (pt, pos');
    1.36  (*val (pt, pos') = generate_inconsistent_rew (sube_opt, thm'_of_thm thm)
    1.37              (fillform, []) (get_loc pt pos) pos' pt*)
    1.38  upd_calc cI ((pt, pos'), []); upd_ipos cI 1 pos';
    1.39 -autocalculateOK2xml cI pos pos' pos';
    1.40  
    1.41  "~~~~~ final check:";
    1.42 -val ((pt,pos),_) = get_calc 1;
    1.43 +val ((pt, _),_) = get_calc 1;
    1.44  val p = get_pos 1 1;
    1.45 -val (Form f, tac, asms) = pt_extract (pt, p);
    1.46 -if p = ([2], Res) andalso term2str f =
    1.47 +val (Form f, _, asms) = pt_extract (pt, p);
    1.48 +if p = ([2], Res) andalso 
    1.49 +  get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", "")) andalso
    1.50 +  term2str f =
    1.51    "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3"
    1.52  then () else error "";
    1.53