src/Pure/Isar/attrib.ML

--- a/src/Pure/Isar/attrib.ML	Fri Feb 10 02:22:39 2006 +0100
+++ b/src/Pure/Isar/attrib.ML	Fri Feb 10 02:22:41 2006 +0100
@@ -27,15 +27,9 @@
     (('c * 'att list) * ('d * 'att list) list) list
   val crude_closure: Context.proof -> src -> src
   val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
-  val global_thm: theory * Args.T list -> thm * (theory * Args.T list)
-  val global_thms: theory * Args.T list -> thm list * (theory * Args.T list)
-  val global_thmss: theory * Args.T list -> thm list * (theory * Args.T list)
-  val local_thm: Context.proof * Args.T list -> thm * (Context.proof * Args.T list)
-  val local_thms: Context.proof * Args.T list -> thm list * (Context.proof * Args.T list)
-  val local_thmss: Context.proof * Args.T list -> thm list * (Context.proof * Args.T list)
   val thm: Context.generic * Args.T list -> thm * (Context.generic * Args.T list)
   val thms: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
-  val thmss: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
+  val multi_thm: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
   val syntax: (Context.generic * Args.T list ->
     attribute * (Context.generic * Args.T list)) -> src -> attribute
   val no_args: attribute -> src -> attribute
@@ -149,37 +143,28 @@
 
 local
 
-fun gen_thm theory_of apply get pick = Scan.depend (fn st =>
- (Scan.ahead Args.alt_name -- Args.named_fact (get st o Fact)
+val get_thms = Context.cases PureThy.get_thms ProofContext.get_thms;
+
+fun gen_thm pick = Scan.depend (fn st =>
+ (Scan.ahead Args.alt_name -- Args.named_fact (get_thms st o Fact)
     >> (fn (s, fact) => ("", Fact s, fact)) ||
-  Scan.ahead Args.name -- Args.named_fact (get st o Name) -- Args.thm_sel
+  Scan.ahead Args.name -- Args.named_fact (get_thms st o Name) -- Args.thm_sel
     >> (fn ((name, fact), sel) => (name, NameSelection (name, sel), fact)) ||
-  Scan.ahead Args.name -- Args.named_fact (get st o Name)
+  Scan.ahead Args.name -- Args.named_fact (get_thms st o Name)
     >> (fn (name, fact) => (name, Name name, fact))) --
-  Args.opt_attribs (intern (theory_of st))
+  Args.opt_attribs (intern (Context.theory_of st))
   >> (fn ((name, thmref, fact), srcs) =>
     let
       val ths = PureThy.select_thm thmref fact;
-      val atts = map (attribute_i (theory_of st)) srcs;
-      val (st', ths') = foldl_map (apply atts) (st, ths);
+      val atts = map (attribute_i (Context.theory_of st)) srcs;
+      val (st', ths') = foldl_map (Library.apply atts) (st, ths);
     in (st', pick name ths') end));
 
-val get_thms = Context.cases PureThy.get_thms ProofContext.get_thms;
-
 in
 
-val global_thm = gen_thm I Thm.theory_attributes PureThy.get_thms PureThy.single_thm;
-val global_thms = gen_thm I Thm.theory_attributes PureThy.get_thms (K I);
-val global_thmss = Scan.repeat global_thms >> List.concat;
-
-val local_thm =
-  gen_thm ProofContext.theory_of Thm.proof_attributes ProofContext.get_thms PureThy.single_thm;
-val local_thms = gen_thm ProofContext.theory_of Thm.proof_attributes ProofContext.get_thms (K I);
-val local_thmss = Scan.repeat local_thms >> List.concat;
-
-val thm = gen_thm Context.theory_of Library.apply get_thms PureThy.single_thm;
-val thms = gen_thm Context.theory_of Library.apply get_thms (K I);
-val thmss = Scan.repeat thms >> List.concat;
+val thm = gen_thm PureThy.single_thm;
+val multi_thm = gen_thm (K I);
+val thms = Scan.repeat multi_thm >> List.concat;
 
 end;
 
@@ -217,7 +202,7 @@
     >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B))));
 
 val OF_att =
-  syntax (thmss >> (fn Bs => Thm.rule_attribute (fn _ => fn A => Bs MRS A)));
+  syntax (thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => Bs MRS A)));
 
 
 (* read_instantiate: named instantiation of type and term variables *)
@@ -397,7 +382,7 @@
 (* unfold / fold definitions *)
 
 fun unfolded_syntax rule =
-  syntax (thmss >>
+  syntax (thms >>
     (fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths)));
 
 val unfolded = unfolded_syntax LocalDefs.unfold;