diff -r 7f242009f7b4 -r 8e8f96dfaf63 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Thu Jun 26 11:58:27 2008 +0200
+++ b/src/Tools/induct.ML	Thu Jun 26 15:06:25 2008 +0200
@@ -718,8 +718,8 @@
       -- Args.term) >> SOME ||
     inst >> Option.map (pair NONE);
 
-val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (context, t) =>
-  error ("Bad free variable: " ^ Syntax.string_of_term (Context.proof_of context) t));
+val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
+  error ("Bad free variable: " ^ Syntax.string_of_term ctxt t));
 
 fun unless_more_args scan = Scan.unless (Scan.lift
   ((Args.$$$ arbitraryN || Args.$$$ takingN || Args.$$$ typeN ||