src/CTT/ex/synth.ML
changeset 17441 5b5feca0344a
parent 9251 bd57acd44fc1
--- a/src/CTT/ex/synth.ML	Fri Sep 16 21:02:15 2005 +0200
+++ b/src/CTT/ex/synth.ML	Fri Sep 16 23:01:29 2005 +0200
@@ -6,7 +6,7 @@
 
 writeln"Synthesis examples, using a crude form of narrowing";
 
-context Arith.thy;
+context (theory "Arith");
 
 writeln"discovery of predecessor function";
 Goal