# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1284395836 -7200
# Node ID 79b6cbd0268127bcfbdf01f35f25bc86708ad892
# Parent  d679c1f837a70b8bfabe6e7bc9dcccf9d330cbb8
tuned

diff -r d679c1f837a7 -r 79b6cbd02681 src/Tools/isac/Build_Isac.thy
--- a/src/Tools/isac/Build_Isac.thy	Mon Sep 13 18:12:15 2010 +0200
+++ b/src/Tools/isac/Build_Isac.thy	Mon Sep 13 18:37:16 2010 +0200
@@ -12,7 +12,7 @@
 header {* Loading the isac mathengine *}
 
 theory Build_Isac
-imports Complex_Main "ProgLang/Language" 
+imports Complex_Main "ProgLang/Language" (*"Knowledge/Test"*)
 begin
 
 ML {* 
@@ -27,9 +27,9 @@
 use "ProgLang/term.sml"
 use "ProgLang/calculate.sml"
 use "ProgLang/rewrite.sml"
-use_thy"ProgLang/Script" (*ListC, Tools, Script*)
+use_thy"ProgLang/Script"    (*ListC, Tools, Script*)
 use "ProgLang/scrtools.sml"
-use_thy"ProgLang/Language"
+use_thy"ProgLang/Language"  (*just for integrating scrtools.sml*)
 
 use "Interpret/mstools.sml"
 use "Interpret/ctree.sml"
@@ -85,6 +85,8 @@
   use_thy "Knowledge/Test"
 *)
 use_thy "Knowledge/Isac"
+check_guhs_unique := false;
+ML {* writeln "**** isac kernel = math-engine + Knowledge complete ******" *}
 
 end