1.1 --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml	Wed Jun 25 13:33:16 2014 +0200
     1.2 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml	Thu Jun 26 10:50:27 2014 +0200
     1.3 @@ -21,7 +21,6 @@
     1.4  "----------- thes2file: thy_containing_rls : rls '...' not in ! --";
     1.5  "----------- fun make_thm ----------------------------------------";
     1.6  "----------- fun insert_fillpats ---------------------------------";
     1.7 -"----------- fun insert_errpatIDs --------------------------------";
     1.8  "--------- (*collect_part: data too large for buffers*) ----------";
     1.9  "----------- collect thydata from Test_Build_Thydata.thy ---------";
    1.10  "----------- correct theIDs for e_rls ----------------------------";
    1.11 @@ -247,41 +246,6 @@
    1.12  (*restore*) insert_fillpats path save_fillpats;
    1.13  ^^^^^--- this intermediate save/restore does not work and affects other tests ---^^*)
    1.14  
    1.15 -"----------- fun insert_errpatIDs --------------------------------";
    1.16 -"----------- fun insert_errpatIDs --------------------------------";
    1.17 -"----------- fun insert_errpatIDs --------------------------------";
    1.18 -(* vv--- this intermediate save/restore does not work and affects other tests ---vv
    1.19 -         see test/../calcelems.sml --- Unsynchronized.ref doesn't work any more ---
    1.20 -
    1.21 -(* isolate test: 10 secs *) val original = (get_thes ());
    1.22 -
    1.23 -(* still ununsed; planned for stepToErrorpattern *)
    1.24 -val path = ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]: theID;
    1.25 -val errpattIDs = ["chain-rule-diff-both", "test-errpatID"];
    1.26 -
    1.27 -insert_errpatIDs path errpattIDs;
    1.28 -
    1.29 -val Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)} = get_the path
    1.30 -val Rls {id, preconds, rew_ord, erls, srls, calc, rules, scr, errpatts} = rls;
    1.31 -
    1.32 -if errpattIDs = ["chain-rule-diff-both", "test-errpatID"] then ()
    1.33 -else error "insert_errpatIDs to norm_diff changed";
    1.34 -
    1.35 -(* isolate test: 10 secs  thehier := original; *)
    1.36 -^^^^^--- this intermediate save/restore does not work and affects other tests ---^^*)
    1.37 -
    1.38 -insert_fillpats @{theory} ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]
    1.39 - ([("fill-d_d-arg",
    1.40 -     parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
    1.41 -   ("fill-both-args",
    1.42 -     parse_patt thy "d_d ?bdv (sin _) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
    1.43 -   ("fill-d_d",
    1.44 -     parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"),
    1.45 -   ("fill-inner-deriv",
    1.46 -     parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),
    1.47 -   ("fill-all",
    1.48 -     parse_patt thy "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list);
    1.49 -
    1.50  "----------- collect_thydata from Test_Build_Thydata.thy ---------";
    1.51  "----------- collect_thydata from Test_Build_Thydata.thy ---------";
    1.52  "----------- collect_thydata from Test_Build_Thydata.thy ---------";