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