| changeset 32010 | cb1a1c94b4cd |
| parent 29291 | d3cc5398bad5 |
| child 32740 | 9dd0a2f83429 |
--- 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'; *}