src/Tools/induct.ML

   ((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME)
       -- Args.term) >> SOME ||
     inst >> Option.map (pair NONE);
 
 val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (context, t) =>
-  error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of context) t));
+  error ("Bad free variable: " ^ Syntax.string_of_term (Context.proof_of context) t));
 
 fun unless_more_args scan = Scan.unless (Scan.lift
   ((Args.$$$ arbitraryN || Args.$$$ takingN || Args.$$$ typeN ||
     Args.$$$ predN || Args.$$$ setN || Args.$$$ ruleN) -- Args.colon)) scan;