1.1 --- a/test/Tools/isac/Interpret/mathengine.sml	Tue Oct 18 12:05:03 2016 +0200
     1.2 +++ b/test/Tools/isac/Interpret/mathengine.sml	Thu Oct 20 10:26:29 2016 +0200
     1.3 @@ -643,12 +643,12 @@
     1.4  "~~~~~ fun generate1, args:"; val (thy, (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))), 
     1.5    (is, ctxt), (p,p_), pt) = ((assoc_thy "Isac"), tac_, is, pos, pt);
     1.6          val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
     1.7 -          (Rewrite (thm'_to_thm'' thm')) (f',asm) Complete;
     1.8 +          (Rewrite thm') (f',asm) Complete;
     1.9  (* in pt: tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
    1.10                                                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
    1.11  "~~~~~ fun cappend_atomic, args:"; val (pt, p, ist_res, f, r, f', s) = 
    1.12 -  (pt, p, (is, insert_assumptions asm ctxt), f, (Rewrite (thm'_to_thm'' thm')), (f',asm), Complete);
    1.13 -existpt p pt andalso get_obj g_tac pt p=Empty_Tac = false;
    1.14 +  (pt, p, (is, insert_assumptions asm ctxt), f, (Rewrite thm'), (f',asm), Complete);
    1.15 +existpt p pt andalso is_empty_tac (get_obj g_tac pt p) = false;
    1.16  apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
    1.17  apfst : ('a -> 'b) -> 'a * 'c -> 'b * 'c;
    1.18  (append_atomic p ist_res f r f' s) : ptree -> ptree;
    1.19 @@ -664,7 +664,7 @@
    1.20  "~~~~~ fun thm'2xml, args:"; val (j, ((ID, form) : thm'')) = ((j+i), thm');
    1.21  ID = "rnorm_equation_add";
    1.22  @{thm rnorm_equation_add};
    1.23 -term2str form = "~ ?b =!= 0 ==> (?a = ?b) = (?a + -1 * ?b = 0)"
    1.24 +(term2str o Thm.prop_of) form = "~ ?b =!= 0 ==> (?a = ?b) = (?a + -1 * ?b = 0)"
    1.25    (*?!? should be "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + -1 * ?b = 0)"*)
    1.26  (*thmstr2xml (j+i) form;
    1.27  ERROR Undeclared constant: "Test.rnorm_equation_add" ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)