# HG changeset patch
# User haftmann
# Date 1162560160 -3600
# Node ID c8cc6b68759fe27a32161afc858e4b4b04e4f377
# Parent  8288c8f203de228e2bf93b7ed1f7af866079af1d
improved evaluation setup

diff -r 8288c8f203de -r c8cc6b68759f src/HOL/ex/CodeEval.thy
--- a/src/HOL/ex/CodeEval.thy	Fri Nov 03 14:22:39 2006 +0100
+++ b/src/HOL/ex/CodeEval.thy	Fri Nov 03 14:22:40 2006 +0100
@@ -116,9 +116,6 @@
 
 subsection {* Evaluation infrastructure *}
 
-lemma lift_eq_Trueprop:
-  "p == q \<Longrightarrow> Trueprop p == Trueprop q" by auto
-
 ML {*
 signature EVAL =
 sig
@@ -144,8 +141,6 @@
     val t = eval_term thy (Sign.read_term thy t);
   in (writeln o Sign.string_of_term thy) t end;
 
-val lift_eq_Trueprop = thm "lift_eq_Trueprop";
-
 exception Eval of term;
 
 val oracle = ("Eval", fn (thy, Eval t) =>
@@ -156,14 +151,10 @@
 fun conv ct =
   let
     val {thy, t, ...} = rep_cterm ct;
-    val t' = HOLogic.dest_Trueprop t;
-    val thm' = Thm.invoke_oracle_i thy oracle_name (thy, Eval t');
-  in
-    lift_eq_Trueprop OF [thm']
-  end;
+  in Thm.invoke_oracle_i thy oracle_name (thy, Eval t) end;
 
 fun tac i = Tactical.PRIMITIVE (Drule.fconv_rule
-  (Drule.goals_conv (equal i) conv));
+  (Drule.goals_conv (equal i) (HOL.Trueprop_conv conv)));
 
 val method =
   Method.no_args (Method.METHOD (fn _ =>