Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/Term_Of_Syntax.thy
changeset 31139 0b615ac7eeaf
parent 28965 1de908189869 
--- 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})
isabelle