1.1 --- a/test/Tools/isac/Test_Isac.thy	Thu Nov 17 16:40:27 2016 +0100
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Mon Nov 21 12:47:02 2016 +0100
     1.3 @@ -20,12 +20,14 @@
     1.4  
     1.5  In order to maintain these tests without changes, this has to be done before running tests:
     1.6  (1) Query replace in src/Tools/isac:
     1.7 -    "--- ! aktivate for Test_Isac BEGIN ---\* )" --> "--- ! aktivate for Test_Isac BEGIN ---\*)"
     1.8 -    "( *\--- ! aktivate for Test_Isac END ---"   --> "(*\--- ! aktivate for Test_Isac END ---"
     1.9 +    "--- ! aktivate for Test_Isac BEGIN ---\* )" \<longrightarrow> "--- ! aktivate for Test_Isac BEGIN ---\*)"
    1.10 +    "( *\--- ! aktivate for Test_Isac END ---"   \<longrightarrow> "(*\--- ! aktivate for Test_Isac END ---"
    1.11    This extends the signatures with some functions required for some tests.
    1.12  
    1.13  Running Test_Isac.thy opens all structures, see code after "begin" below.
    1.14  
    1.15 +*   before running Test_Isac.thy  ^^^            \<longrightarrow>  ^^^  in src/Tools/isac
    1.16 +*   after running Test_Isac.thy   ^^^            <--  ^^^  in src/Tools/isac
    1.17  *********************** DON'T FORGET TO REVERSE CHANGE (1) AFTER TESTS ***********************
    1.18  \<close>
    1.19  
    1.20 @@ -65,6 +67,7 @@
    1.21  ML {*
    1.22  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    1.23    open Lucin;
    1.24 +  open Kernel;
    1.25  (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.26  *}
    1.27  ML {*