src/Tools/isac/Test_Isac.thy
branchdecompose-isar
changeset 40836 69364e021751
parent 38085 45de545f1699
child 41924 7407ceef2aed
     1.1 --- a/src/Tools/isac/Test_Isac.thy	Tue Jan 11 15:28:03 2011 +0100
     1.2 +++ b/src/Tools/isac/Test_Isac.thy	Mon Feb 21 19:40:36 2011 +0100
     1.3 @@ -125,7 +125,7 @@
     1.4  	use"algein.sml";
     1.5  *)
     1.6  ML {*
     1.7 -theory "Isac"
     1.8 +Thy_Info.get_theory "Isac"
     1.9  *}
    1.10  use "../../../test/Tools/isac/Knowledge/isac.sml"; (**)
    1.11  
    1.12 @@ -139,7 +139,7 @@
    1.13  use_thy "../../Tools/isac/ADDTESTS/file-depend/Build_Test"
    1.14  :
    1.15  *** Could not find theory file "Foo_Language.thy" in "1language", "/usr/local/isabisac/test/Tools/isac", ".", "$ISABELLE_HOME/src/HOL/Library"
    1.16 -*** Theory loader: the error(s) above occurred while examining theory "Foo_Language"
    1.17 +*** Theory loader: the error(s) above occurred while examining Thy_Info.get_theory "Foo_Language"
    1.18  
    1.19  use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test"
    1.20  *)