src/Pure/Isar/obtain.ML

     val vs = map (dest_Free o Thm.term_of) xs;
     val bads = Term.fold_aterms (fn t as Free v =>
       if member (op =) vs v then insert (op aconv) t else I | _ => I) tm [];
     val _ = null bads orelse
       error ("Result contains obtained parameters: " ^
-        space_implode " " (map (ProofContext.string_of_term ctxt) bads));
+        space_implode " " (map (Syntax.string_of_term ctxt) bads));
   in tm end;
 
 fun eliminate fix_ctxt rule xs As thm =
   let
     val thy = ProofContext.theory_of fix_ctxt;

 fun unify_params vars thesis_var raw_rule ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
     val certT = Thm.ctyp_of thy;
     val cert = Thm.cterm_of thy;
-    val string_of_typ = ProofContext.string_of_typ ctxt;
-    val string_of_term = setmp show_types true (ProofContext.string_of_term ctxt);
+    val string_of_typ = Syntax.string_of_typ ctxt;
+    val string_of_term = setmp show_types true (Syntax.string_of_term ctxt);
 
     fun err msg th = error (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th);
 
     val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1;
     val rule = Thm.incr_indexes (maxidx + 1) raw_rule;