--- a/src/HOL/Library/Eval_Witness.thy Thu Oct 04 16:59:30 2007 +0200
+++ b/src/HOL/Library/Eval_Witness.thy Thu Oct 04 19:41:49 2007 +0200
@@ -57,12 +57,11 @@
| dest_exs n (Const ("Ex", _) $ Abs (v,T,b)) =
Abs (v, check_type T, dest_exs (n - 1) b)
| dest_exs _ _ = sys_error "dest_exs";
-
- val ct = Thm.cterm_of thy (dest_exs (length ws) (HOLogic.dest_Trueprop goal))
+ val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
in
- if CodePackage.satisfies thy ct ws
+ if CodePackage.satisfies thy t ws
then goal
- else HOLogic.Trueprop $ (HOLogic.true_const) (*dummy*)
+ else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
end
*}