src/HOL/Tools/Predicate_Compile/code_prolog.ML

   let
     val ctxt = Toplevel.context_of state
     val t = Syntax.read_term ctxt raw_t
     val t' = values ctxt soln t
     val ty' = Term.type_of t'
-    val ctxt' = Variable.auto_fixes t' ctxt
+    val ctxt' = Proof_Context.augment t' ctxt
     val _ = tracing "Printing terms..."
   in
     Print_Mode.with_modes print_modes (fn () =>
       Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ()