src/HOL/Tools/Predicate_Compile/code_prolog.ML
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 () =>