test/Tools/isac/ADDTESTS/file-depend/2interpreter/2foointerpreter.ML
branchdecompose-isar
changeset 41905 b772eb34c16c
parent 41899 d837e83a4835
child 41922 32d7766945fb
     1.1 --- a/test/Tools/isac/ADDTESTS/file-depend/2interpreter/2foointerpreter.ML	Sat Feb 26 12:53:00 2011 +0100
     1.2 +++ b/test/Tools/isac/ADDTESTS/file-depend/2interpreter/2foointerpreter.ML	Tue Mar 01 15:23:59 2011 +0100
     1.3 @@ -3,7 +3,9 @@
     1.4  fun foointerpret ((Const ("Foo_Language.fooprog", _)) $ (_ $ _ $ res)) = res;
     1.5  
     1.6  (* Foo_Language's definitions are recognized: *)
     1.7 -val trm = Syntax.read_term_global @{theory Foo_Language} "fooprog (a = b)";
     1.8 +(*val trm = Syntax.read_term_global @{theory Foo_Language} "fooprog (a = b)"; *)
     1.9 +val trm = Syntax.read_term_global @{theory "../1language/Foo_Language"} 
    1.10 +                                       "fooprog (a = b)";
    1.11  (*val trm =
    1.12     Const ("Foo_Language.fooprog", "bool => Foo_Language.foosource") $
    1.13       (Const ("op =", "'a => 'a => bool") $ Free ("a", "'a") $