src/Pure/Isar/args.ML

   val term_abbrev: Context.generic * T list -> term * (Context.generic * T list)
   val prop: Context.generic * T list -> term * (Context.generic * T list)
   val tyname: Context.generic * T list -> string * (Context.generic * T list)
   val const: Context.generic * T list -> string * (Context.generic * T list)
   val const_proper: Context.generic * T list -> string * (Context.generic * T list)
-  val thm_sel: T list -> PureThy.interval list * T list
+  val thm_sel: T list -> Facts.interval list * T list
   val bang_facts: Context.generic * T list -> thm list * (Context.generic * T list)
   val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list)
     -> ((int -> tactic) -> tactic) * ('a * T list)
   val attribs: (string -> string) -> T list -> src list * T list
   val opt_attribs: (string -> string) -> T list -> src list * T list

 
 
 (* misc *)
 
 val thm_sel = parens (list1
- (nat --| $$$ "-" -- nat >> PureThy.FromTo ||
-  nat --| $$$ "-" >> PureThy.From ||
-  nat >> PureThy.Single));
+ (nat --| $$$ "-" -- nat >> Facts.FromTo ||
+  nat --| $$$ "-" >> Facts.From ||
+  nat >> Facts.Single));
 
 val bang_facts = Scan.peek (fn context =>
   $$$ "!" >> (fn _ => (warning "use of prems in proof method";
     Assumption.prems_of (Context.proof_of context))) || Scan.succeed []);