--- a/src/Tools/induct.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Tools/induct.ML Tue Oct 09 00:20:13 2007 +0200
@@ -718,7 +718,7 @@
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 ||