--- a/src/Pure/Isar/args.ML Thu Jun 26 15:06:25 2008 +0200
+++ b/src/Pure/Isar/args.ML Thu Jun 26 15:06:28 2008 +0200
@@ -35,6 +35,8 @@
val assignable: src -> src
val assign: value option -> T -> unit
val closure: src -> src
+ val context: Context.generic * T list -> Context.proof * (Context.generic * T list)
+ val theory: Context.generic * T list -> Context.theory * (Context.generic * T list)
val position: (T list -> 'a * 'b) -> T list -> ('a * Position.T) * 'b
val !!! : (T list -> 'a) -> T list -> 'a
val $$$ : string -> T list -> string * T list
@@ -224,6 +226,12 @@
(** scanners **)
+(* context *)
+
+fun context x = (Scan.state >> Context.proof_of) x;
+fun theory x = (Scan.state >> Context.theory_of) x;
+
+
(* position *)
fun position scan =