diff -r a51ce445d498 -r 0b615ac7eeaf src/HOL/ex/Term_Of_Syntax.thy
--- a/src/HOL/ex/Term_Of_Syntax.thy	Wed May 13 18:41:40 2009 +0200
+++ b/src/HOL/ex/Term_Of_Syntax.thy	Wed May 13 18:41:54 2009 +0200
@@ -31,9 +31,9 @@
 
 setup {*
 let
-  val subst_rterm_of = Eval.mk_term
-    (fn (v, _) => error ("illegal free variable in term quotation: " ^ quote v))
-    (Typerep.mk (fn (v, sort) => Typerep.typerep (TFree (v, sort))));
+  val subst_rterm_of = map_aterms
+    (fn Free (v, _) => error ("illegal free variable in term quotation: " ^ quote v) | t => t)
+      o HOLogic.reflect_term;
   fun subst_rterm_of' (Const (@{const_name rterm_of}, _), [t]) = subst_rterm_of t
     | subst_rterm_of' (Const (@{const_name rterm_of}, _), _) =
         error ("illegal number of arguments for " ^ quote @{const_name rterm_of})