Adapted to Context.generic syntax.
authorberghofe
Mon Feb 13 17:02:54 2006 +0100 (2006-02-13)
changeset 1903673782d21e855
parent 19035 678ef6658a0e
child 19037 3be721728a6c
Adapted to Context.generic syntax.
src/HOL/Nominal/nominal_induct.ML
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Mon Feb 13 14:05:43 2006 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Mon Feb 13 17:02:54 2006 +0100
     1.3 @@ -125,15 +125,15 @@
     1.4  val fixingN = "fixing";
     1.5  val ruleN = "rule";
     1.6  
     1.7 -val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.local_term >> SOME;
     1.8 +val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
     1.9  
    1.10  val def_inst =
    1.11    ((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME)
    1.12 -      -- Args.local_term) >> SOME ||
    1.13 +      -- Args.term) >> SOME ||
    1.14      inst >> Option.map (pair NONE);
    1.15  
    1.16 -val free = Scan.state -- Args.local_term >> (fn (_, Free v) => v | (ctxt, t) =>
    1.17 -  error ("Bad free variable: " ^ ProofContext.string_of_term ctxt t));
    1.18 +val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
    1.19 +  error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of ctxt) t));
    1.20  
    1.21  fun unless_more_args scan = Scan.unless (Scan.lift
    1.22    ((Args.$$$ avoidingN || Args.$$$ fixingN || Args.$$$ ruleN) -- Args.colon)) scan;
    1.23 @@ -145,7 +145,7 @@
    1.24  val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN -- Args.colon) |--
    1.25    Args.and_list (Scan.repeat (unless_more_args free))) [];
    1.26  
    1.27 -val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.local_thmss;
    1.28 +val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms;
    1.29  
    1.30  in
    1.31