src/HOL/Code_Evaluation.thy

--- a/src/HOL/Code_Evaluation.thy	Sat Jun 01 14:26:04 2013 +0200
+++ b/src/HOL/Code_Evaluation.thy	Sun Jun 02 07:46:40 2013 +0200
@@ -165,6 +165,11 @@
   (Eval "Code'_Evaluation.tracing")
 
 
+subsection {* Generic reification *}
+
+ML_file "~~/src/HOL/Tools/reification.ML"
+
+
 hide_const dummy_term valapp
 hide_const (open) Const App Abs Free termify valtermify term_of tracing