# HG changeset patch
# User berghofe
# Date 1139846574 -3600
# Node ID 73782d21e855b9010b7ce6d6efdf9a2518e317fa
# Parent  678ef6658a0e1812376518535292cfc8701485e2
Adapted to Context.generic syntax.

diff -r 678ef6658a0e -r 73782d21e855 src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Mon Feb 13 14:05:43 2006 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Mon Feb 13 17:02:54 2006 +0100
@@ -125,15 +125,15 @@
 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;
@@ -145,7 +145,7 @@
 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