1.1 --- a/test/Tools/isac/Interpret/rewtools.sml	Tue Oct 18 12:05:03 2016 +0200
     1.2 +++ b/test/Tools/isac/Interpret/rewtools.sml	Thu Oct 20 10:26:29 2016 +0200
     1.3 @@ -180,7 +180,7 @@
     1.4  "----------- checkContext..Thy_, fun context_thy --------";
     1.5  (*using pt from above*)
     1.6  val p = ([2,4], Res);
     1.7 -val tac = Rewrite ("radd_left_commute", e_term);
     1.8 +val tac = Rewrite ("radd_left_commute", @{thm radd_left_commute});
     1.9  checkContext 1 p "thy_Test-thm-radd_left_commute";
    1.10  (* radd_left_commute: 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0
    1.11    --- in checkContext..Thy_ ---*)
    1.12 @@ -190,13 +190,13 @@
    1.13  else error "rewtools.sml checkContext.._ thy_Test-thm-radd_left_commute";
    1.14  
    1.15  val p = ([3,1,1], Frm);
    1.16 -val tac = Rewrite_Inst (["(bdv,x)"],("risolate_bdv_add", e_term));
    1.17 +val tac = Rewrite_Inst (["(bdv,x)"],("risolate_bdv_add", @{thm "risolate_bdv_add"}));
    1.18  checkContext 1 p "thy_Test-thm-risolate_bdv_add";
    1.19  (* risolate_bdv_add:  -1 + x = 0 -> x = 0 + -1 * -1
    1.20    --- in checkContext..Thy_ ---*)
    1.21  val ContThmInst {thm,result,...} = context_thy (pt,p) tac;
    1.22  if thm =  "thy_isac_Test-thm-risolate_bdv_add"
    1.23 -   andalso term2str result = "x = 0 + -1 * -1" then ()
    1.24 +   andalso term2str result = "x = 0 + - 1 * -1" then ()
    1.25  else error "rewtools.sml checkContext..T_ thy_Test-thm-risolate_bdv_add";
    1.26  
    1.27  val p = ([2,5], Res);
    1.28 @@ -452,5 +452,3 @@
    1.29  | _ => error "get_bdv_subst changed 3";
    1.30  
    1.31  val (SOME subs, _) = get_bdv_subst prog env;
    1.32 -Rewrite_Inst (subs, ("diff_sin_chain", e_term)) (*<<<----- this is the intended usage*)
    1.33 -