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/Library/reflection.ML
changeset 42284 326f57825e1a
parent 38864 4abe644fcea5
child 42361 23f352990944 
--- a/src/HOL/Library/reflection.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Library/reflection.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -125,7 +125,7 @@
              Abs(xn,xT,ta) => (
                let
                  val ([xn],ctxt') = Variable.variant_fixes ["x"] ctxt
-                 val (xn,ta) = variant_abs (xn,xT,ta)
+                 val (xn,ta) = Syntax_Trans.variant_abs (xn,xT,ta)  (* FIXME !? *)
                  val x = Free(xn,xT)
                  val bds = (case AList.lookup Type.could_unify bds (HOLogic.listT xT)
                           of NONE => error "tryabsdecomp: Type not found in the Environement"
isabelle