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") $