1.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Sun Jun 22 15:17:07 2014 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Sun Jun 22 15:22:30 2014 +0200
     1.3 @@ -3,7 +3,8 @@
     1.4   *)
     1.5  
     1.6  theory Build_Thydata
     1.7 -imports Isac "~~/src/Tools/isac/ProgLang/ProgLang" 
     1.8 +imports 
     1.9 +  Isac "~~/src/Tools/isac/Interpret/Interpret"
    1.10    Test_Build_Thydata (*for test/../build_thydata.sml, thy_hierarchy.sml*)
    1.11  begin
    1.12  

     2.1 --- a/src/Tools/isac/Knowledge/DiffApp.sml	Sun Jun 22 15:17:07 2014 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/DiffApp.sml	Sun Jun 22 15:22:30 2014 +0200
     2.3 @@ -3,7 +3,6 @@
     2.4  *)
     2.5  
     2.6  
     2.7 -theory' := overwritel (!theory', [("DiffAppl",DiffAppl.thy)]);
     2.8  
     2.9  (* 
    2.10  > get_pbt ["DiffAppl","maximum_of","function"];

     3.1 --- a/src/Tools/isac/Knowledge/InsSort.sml	Sun Jun 22 15:17:07 2014 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/InsSort.sml	Sun Jun 22 15:22:30 2014 +0200
     3.3 @@ -20,7 +20,6 @@
     3.4  
     3.5  (*-------------------------from InsSort.ML 8.3.01----------------------*)
     3.6  
     3.7 -theory' := (!theory') @ [("InsSort",InsSort.thy)];
     3.8  
     3.9  val ins_sort = 
    3.10    Rls{preconds = [], rew_ord = ("tless_true",tless_true),

     4.1 --- a/src/Tools/isac/Knowledge/Isac.thy	Sun Jun 22 15:17:07 2014 +0200
     4.2 +++ b/src/Tools/isac/Knowledge/Isac.thy	Sun Jun 22 15:22:30 2014 +0200
     4.3 @@ -25,32 +25,4 @@
     4.4  
     4.5  ML {* val version_isac = "isac version 120504 15:33"; *}
     4.6  
     4.7 -ML {* (* there are strange dependencies between tests:
     4.8 -         insert_fillpats in test/../thy_hierarchy.sml affects subsequent tests,
     4.9 -         see changeset 58e0a39e58b7.
    4.10 -         This function checks for data in ! mets, get_thes () set in Build_Thydata.thy *)
    4.11 -
    4.12 -fun check_unsynchronized_ref () =
    4.13 -  let
    4.14 -    val met = get_met ["diff","differentiate_on_R"];
    4.15 -    val {errpats, ...} = met;
    4.16 -    val hthm = get_the ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"];
    4.17 -    val Hthm {fillpats, ...} = hthm;
    4.18 -    val hrls = get_the ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"];
    4.19 -    val Hrls {thy_rls = (thyID, rls), ...} = hrls
    4.20 -    val Rls {errpatts, ...} = rls;
    4.21 -  in
    4.22 -    case errpats of
    4.23 -      ("chain-rule-diff-both", _ :: _,_ :: _) :: _ => writeln "----- errpats original"
    4.24 -    | _ => writeln "##### errpats changed";
    4.25 -    case fillpats of
    4.26 -      ("fill-d_d-arg", _, "chain-rule-diff-both") :: ("fill-both-args", _, "chain-rule-diff-both") :: _ 
    4.27 -        => writeln "----- fillpats original"
    4.28 -    | _ => writeln "##### fillpats changed";
    4.29 -    case errpatts of 
    4.30 -      ["chain-rule-diff-both", "cancel"] => writeln "----- errpatIDs original"
    4.31 -    | _ => writeln "##### errpatIDs changed"
    4.32 -  end;
    4.33 -*}
    4.34 -
    4.35  end

     5.1 --- a/src/Tools/isac/ROOT	Sun Jun 22 15:17:07 2014 +0200
     5.2 +++ b/src/Tools/isac/ROOT	Sun Jun 22 15:22:30 2014 +0200
     5.3 @@ -9,7 +9,7 @@
     5.4    ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
     5.5  before out-outcommenting (*, browser_info = true*) below and ...
     5.6  $ ./bin/isabelle build -o browser_info -v -c HOL
     5.7 -$ ./bin/isabelle build -o browser_info -d src/Tools/isac/ -v -b Isac
     5.8 +$ ./bin/isabelle build -o browser_info -d src/Tools/isac/ -v -b Isac     ERROR: duplicate session Isac ?!?
     5.9  *)
    5.10  
    5.11  session Isac in "~~/src/Tools/isac" = HOL +

     6.1 --- a/src/Tools/isac/calcelems.sml	Sun Jun 22 15:17:07 2014 +0200
     6.2 +++ b/src/Tools/isac/calcelems.sml	Sun Jun 22 15:22:30 2014 +0200
     6.3 @@ -953,8 +953,6 @@
     6.4  	  | nodes coll (n::ns) = (node coll n) @ (nodes coll ns);
     6.5      in nodes [] mets end;
     6.6  
     6.7 -(* val (guh, mets) = ("met_test", !mets);
     6.8 -   *)
     6.9  fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) =
    6.10      if member op = (coll_metguhs mets) guh
    6.11      then error ("check_guh_unique failed with '"^guh^"';\n"^

     7.1 --- a/test/Tools/isac/Interpret/mathengine.sml	Sun Jun 22 15:17:07 2014 +0200
     7.2 +++ b/test/Tools/isac/Interpret/mathengine.sml	Sun Jun 22 15:22:30 2014 +0200
     7.3 @@ -1,6 +1,11 @@
     7.4  (* Title:  tests for Interpret/mathengine.sml
     7.5     Author: Walther Neuper 2000, 2006
     7.6     (c) due to copyright terms
     7.7 +
     7.8 +theory Test_Some imports Build_Thydata begin 
     7.9 +ML {* KEStore_Elems.set_ref_thy @{theory};
    7.10 +  fun autoCalculate' cI auto = autoCalculate cI auto |> Future.join *}
    7.11 +ML_file "~~/test/Tools/isac/Interpret/mathengine.sml"
    7.12  *)
    7.13  "--------------------------------------------------------";
    7.14  "table of contents --------------------------------------";