src/HOL/Statespace/DistinctTreeProver.thy

                in (da := thm; thy') end)
 *}
 
 
 ML {* 
- val ct' = cterm_of (the_context ()) t';
+ val ct' = cterm_of @{theory} t';
 *}
 
 ML {*
  timeit (fn () => (DistinctTreeProver.subtractProver (term_of ct') ct' (!da);())) 
 *}

 
 
 
 
 ML {*
-val cdist' = cterm_of (the_context ()) dist';
+val cdist' = cterm_of @{theory} dist';
 DistinctTreeProver.distinct_implProver (!da) cdist';
 *}
 
 *)