# HG changeset patch
# User wenzelm
# Date 1214485585 -7200
# Node ID 8e8f96dfaf639b8a5c3c2e6a574cdd8aed998d13
# Parent  7f242009f7b45dd2413e66e90c93a64cf113cefb
Args.context;

diff -r 7f242009f7b4 -r 8e8f96dfaf63 src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Thu Jun 26 11:58:27 2008 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML	Thu Jun 26 15:06:25 2008 +0200
@@ -134,8 +134,8 @@
       -- Args.term) >> SOME ||
     inst >> Option.map (pair NONE);
 
-val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
-  error ("Bad free variable: " ^ Syntax.string_of_term (Context.proof_of ctxt) 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.$$$ avoidingN || Args.$$$ fixingN || Args.$$$ ruleN) -- Args.colon)) scan;
diff -r 7f242009f7b4 -r 8e8f96dfaf63 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Thu Jun 26 11:58:27 2008 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Thu Jun 26 15:06:25 2008 +0200
@@ -58,9 +58,6 @@
 
 (** concrete antiquotations **)
 
-fun context x = (Scan.state >> Context.proof_of) x;
-
-
 (* misc *)
 
 val _ = value "theory"
@@ -74,7 +71,7 @@
 
 val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
 
-val _ = inline "sort" (context -- Scan.lift Args.name >> (fn (ctxt, s) =>
+val _ = inline "sort" (Args.context -- Scan.lift Args.name >> (fn (ctxt, s) =>
   ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))));
 
 val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
@@ -91,11 +88,11 @@
   "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
 
 val _ = value "cpat"
-  (context -- Scan.lift Args.name >> uncurry ProofContext.read_term_pattern >> (fn t =>
+  (Args.context -- Scan.lift Args.name >> uncurry ProofContext.read_term_pattern >> (fn t =>
     "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
 
 
-fun type_ syn = (context -- Scan.lift Args.name >> (fn (ctxt, c) =>
+fun type_ syn = (Args.context -- Scan.lift Args.name >> (fn (ctxt, c) =>
     #1 (Term.dest_Type (ProofContext.read_tyname ctxt c))
     |> syn ? Sign.base_name
     |> ML_Syntax.print_string));
@@ -104,7 +101,7 @@
 val _ = inline "type_syntax" (type_ true);
 
 
-fun const syn = context -- Scan.lift Args.name >> (fn (ctxt, c) =>
+fun const syn = Args.context -- Scan.lift Args.name >> (fn (ctxt, c) =>
   #1 (Term.dest_Const (ProofContext.read_const_proper ctxt c))
   |> syn ? ProofContext.const_syntax_name ctxt
   |> ML_Syntax.print_string);
@@ -113,7 +110,7 @@
 val _ = inline "const_syntax" (const true);
 
 val _ = inline "const"
-  (context -- Scan.lift Args.name --
+  (Args.context -- Scan.lift Args.name --
     Scan.optional (Scan.lift (Args.$$$ "(") |-- Args.enum1 "," Args.typ --| Scan.lift (Args.$$$ ")")) []
     >> (fn ((ctxt, c), Ts) =>
       let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c)
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 ||