diff -r 53d21039518a -r 7f568724d67e src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Jun 03 14:47:27 2019 +0200 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Jun 03 15:40:08 2019 +0200 @@ -1018,7 +1018,7 @@ 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 () =>