diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/Statespace/DistinctTreeProver.thy
--- a/src/HOL/Statespace/DistinctTreeProver.thy	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Statespace/DistinctTreeProver.thy	Wed Jul 15 23:48:21 2009 +0200
@@ -676,7 +676,7 @@
 
 
 ML {* 
- val ct' = cterm_of (the_context ()) t';
+ val ct' = cterm_of @{theory} t';
 *}
 
 ML {*
@@ -706,7 +706,7 @@
 
 
 ML {*
-val cdist' = cterm_of (the_context ()) dist';
+val cdist' = cterm_of @{theory} dist';
 DistinctTreeProver.distinct_implProver (!da) cdist';
 *}