| changeset 70308 | 7f568724d67e |
| parent 69593 | 3dda49e08b9d |
| child 73233 | 4d36070bdbf4 |
--- 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 () =>