src/Pure/Isar/proof_context.ML

--- a/src/Pure/Isar/proof_context.ML	Fri Jan 11 00:29:25 2002 +0100
+++ b/src/Pure/Isar/proof_context.ML	Fri Jan 11 00:29:54 2002 +0100
@@ -83,8 +83,11 @@
   val put_thmss: (string * thm list) list -> context -> context
   val reset_thms: string -> context -> context
   val have_thmss:
-    ((string * context attribute list) * (thm list * context attribute list) list) list ->
-      context -> context * (string * thm list) list
+    ((bstring * context attribute list) * (xstring * context attribute list) list) list ->
+      context -> context * (bstring * thm list) list
+  val have_thmss_i:
+    ((bstring * context attribute list) * (thm list * context attribute list) list) list ->
+      context -> context * (bstring * thm list) list
   val export_assume: exporter
   val export_presume: exporter
   val cert_def: context -> term -> string * term
@@ -962,16 +965,25 @@
 
 (* have_thmss *)
 
-fun have_thss (ctxt, ((name, more_attrs), ths_attrs)) =
+local
+
+fun gen_have_thss get (ctxt, ((name, more_attrs), ths_attrs)) =
   let
     fun app ((ct, ths), (th, attrs)) =
-      let val (ct', th') = Thm.applys_attributes ((ct, th), attrs @ more_attrs)
-      in (ct', th' :: ths) end
+      let val (ct', th') = Thm.applys_attributes ((ct, get ctxt th), attrs @ more_attrs)
+      in (ct', th' :: ths) end;
     val (ctxt', rev_thms) = foldl app ((ctxt, []), ths_attrs);
     val thms = flat (rev rev_thms);
   in (ctxt' |> put_thms (name, thms), (name, thms)) end;
 
-fun have_thmss args ctxt = foldl_map have_thss (ctxt, args);
+fun gen_have_thmss get args ctxt = foldl_map (gen_have_thss get) (ctxt, args);
+
+in
+
+val have_thmss = gen_have_thmss get_thms;
+val have_thmss_i = gen_have_thmss (K I);
+
+end;
 
 
 
@@ -1035,7 +1047,7 @@
     val (ctxt', [(_, thms)]) =
       ctxt
       |> auto_bind_facts props
-      |> have_thmss [((name, attrs), ths)];
+      |> have_thmss_i [((name, attrs), ths)];
   in (ctxt', (cprops, (name, asms), (name, thms))) end;
 
 fun gen_assms prepp exp args ctxt =