src/HOL/Nominal/nominal_induct.ML

 
 val avoidingN = "avoiding";
 val fixingN = "fixing";
 val ruleN = "rule";
 
-val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.local_term >> SOME;
+val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
 
 val def_inst =
   ((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME)
-      -- Args.local_term) >> SOME ||
+      -- Args.term) >> SOME ||
     inst >> Option.map (pair NONE);
 
-val free = Scan.state -- Args.local_term >> (fn (_, Free v) => v | (ctxt, t) =>
-  error ("Bad free variable: " ^ ProofContext.string_of_term ctxt t));
+val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
+  error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of ctxt) t));
 
 fun unless_more_args scan = Scan.unless (Scan.lift
   ((Args.$$$ avoidingN || Args.$$$ fixingN || Args.$$$ ruleN) -- Args.colon)) scan;
 
 

   Scan.repeat (unless_more_args free)) [];
 
 val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN -- Args.colon) |--
   Args.and_list (Scan.repeat (unless_more_args free))) [];
 
-val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.local_thmss;
+val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms;
 
 in
 
 fun nominal_induct_method src =
   Method.syntax