1.1 --- a/test/Tools/isac/Test_Isac.thy	Fri Jun 21 08:06:50 2013 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Fri Jun 21 11:19:18 2013 +0200
     1.3 @@ -124,8 +124,8 @@
     1.4    use "Interpret/mstools.sml"
     1.5    use "Interpret/ctree.sml"         (*!...!see(25)*)
     1.6    use "Interpret/ptyps.sml"
     1.7 -  ML {* check_unsynchronized_ref (); (*==== trick on error: CUT AND PASTE THIS LINE =========*) *}
     1.8 -(*get_pbt not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*)
     1.9 +  ML {* (*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*) *}
    1.10 +(*TRICK DOESNÄT WORK: get_pbt not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*)
    1.11    use "Interpret/generate.sml"
    1.12  (*... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
    1.13    use "Interpret/calchead.sml"      (*part.*)
    1.14 @@ -134,6 +134,8 @@
    1.15  (*val it = "----------- fun thy_containing_rls ---------------------": string
    1.16  :
    1.17   thy_containing_rls changed 1                    ...CONCERNED WITH thehier
    1.18 +
    1.19 +!!!!!!!!!!!!!!!!!!!!!!!! THIS TEST RANDOMLY RAISES AN ERROR OR NOT !!!!!!!!!!!!!!!!!!!!!!!!
    1.20  *)
    1.21    use "Interpret/script.sml"        (*!TODO/part.*)
    1.22    use "Interpret/solve.sml"         (*part.*)
    1.23 @@ -149,7 +151,7 @@
    1.24    use "xmlsrc/mathml.sml"            (*part.*)
    1.25    use "xmlsrc/datatypes.sml"         (*TODO/part.*)
    1.26    use "xmlsrc/pbl-met-hierarchy.sml" (*TODO after 2009-2/part.*)
    1.27 -  use "xmlsrc/thy-hierarchy.sml"     (*TODO after 2009-2/part.*)
    1.28 +(*use "xmlsrc/thy-hierarchy.sml"     TODO after 2009-2/part | Isabelle2012-->13 !thehier! *)
    1.29  (*val it = "----------- ### thes2file ... Exception- Match raised -----------": string
    1.30  :
    1.31  val it = "~~~~~ fun thes2file, args:": string