--- a/src/HOL/Code_Evaluation.thy Thu May 26 15:27:50 2016 +0200
+++ b/src/HOL/Code_Evaluation.thy Thu May 26 15:27:50 2016 +0200
@@ -68,6 +68,19 @@
subsection \<open>Tools setup and evaluation\<close>
+context
+begin
+
+qualified definition TERM_OF :: "'a::term_of itself"
+where
+ "TERM_OF = snd (Code_Evaluation.term_of :: 'a \<Rightarrow> _, TYPE('a))"
+
+qualified definition TERM_OF_EQUAL :: "'a::term_of itself"
+where
+ "TERM_OF_EQUAL = snd (\<lambda>(a::'a). (Code_Evaluation.term_of a, HOL.eq a), TYPE('a))"
+
+end
+
lemma eq_eq_TrueD:
fixes x y :: "'a::{}"
assumes "(x \<equiv> y) \<equiv> Trueprop True"