src/Tools/Code/code_thingol.ML
changeset 42284 326f57825e1a
parent 41782 ffcc3137b1ad
child 42359 6ca5407863ed
     1.1 --- a/src/Tools/Code/code_thingol.ML	Fri Apr 08 11:39:45 2011 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Fri Apr 08 13:31:16 2011 +0200
     1.3 @@ -688,7 +688,7 @@
     1.4        pair (IVar (SOME v))
     1.5    | translate_term thy algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) =
     1.6        let
     1.7 -        val (v', t') = Syntax.variant_abs (Name.desymbolize false v, ty, t);
     1.8 +        val (v', t') = Syntax_Trans.variant_abs (Name.desymbolize false v, ty, t);
     1.9          val v'' = if member (op =) (Term.add_free_names t' []) v'
    1.10            then SOME v' else NONE
    1.11        in