# HG changeset patch
# User wenzelm
# Date 1238257271 -3600
# Node ID ac7570d80c3d29edc36a79859d8c97fb1198e8f0
# Parent  0fffc66b10d72a9603d38d68fd216b62039ae7aa
renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;

diff -r 0fffc66b10d7 -r ac7570d80c3d src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Sat Mar 28 17:10:43 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Sat Mar 28 17:21:11 2009 +0100
@@ -156,9 +156,9 @@
         val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
     in
       lthy
-        |> ProofContext.note_thmss_i "" [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd
-        |> ProofContext.note_thmss_i "" [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
-        |> ProofContext.note_thmss_i ""
+        |> ProofContext.note_thmss "" [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd
+        |> ProofContext.note_thmss "" [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
+        |> ProofContext.note_thmss ""
           [((Binding.name "termination", [ContextRules.intro_bang (SOME 0)]),
             [([Goal.norm_result termination], [])])] |> snd
         |> Proof.theorem_i NONE (total_termination_afterqed data) [[(goal, [])]]
diff -r 0fffc66b10d7 -r ac7570d80c3d src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat Mar 28 17:10:43 2009 +0100
+++ b/src/Pure/Isar/attrib.ML	Sat Mar 28 17:21:11 2009 +0100
@@ -123,7 +123,7 @@
 
 fun attribute thy = attribute_i thy o intern_src thy;
 
-fun eval_thms ctxt args = ProofContext.note_thmss_i Thm.theoremK
+fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
     [(Thm.empty_binding, args |> map (fn (a, atts) =>
         (ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt
   |> fst |> maps snd;
diff -r 0fffc66b10d7 -r ac7570d80c3d src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sat Mar 28 17:10:43 2009 +0100
+++ b/src/Pure/Isar/element.ML	Sat Mar 28 17:21:11 2009 +0100
@@ -510,7 +510,7 @@
   | activate_elem (Notes (kind, facts)) ctxt =
       let
         val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
-        val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
+        val (res, ctxt') = ctxt |> ProofContext.note_thmss kind facts';
       in ctxt' end;
 
 fun gen_activate prep_facts raw_elems ctxt =
diff -r 0fffc66b10d7 -r ac7570d80c3d src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Mar 28 17:10:43 2009 +0100
+++ b/src/Pure/Isar/locale.ML	Sat Mar 28 17:21:11 2009 +0100
@@ -325,7 +325,7 @@
   | init_local_elem (Notes (kind, facts)) ctxt =
       let
         val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
-      in ProofContext.note_thmss_i kind facts' ctxt |> snd end
+      in ProofContext.note_thmss kind facts' ctxt |> snd end
 
 fun cons_elem false (Notes notes) elems = elems
   | cons_elem _ elem elems = elem :: elems
diff -r 0fffc66b10d7 -r ac7570d80c3d src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Mar 28 17:10:43 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Sat Mar 28 17:21:11 2009 +0100
@@ -623,7 +623,7 @@
 fun gen_thmss more_facts opt_chain opt_result prep_atts prep_fact args state =
   state
   |> assert_forward
-  |> map_context_result (ProofContext.note_thmss_i ""
+  |> map_context_result (ProofContext.note_thmss ""
     (Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state)) args))
   |> these_factss (more_facts state)
   ||> opt_chain
@@ -655,7 +655,7 @@
   state
   |> assert_backward
   |> map_context_result
-    (ProofContext.note_thmss_i ""
+    (ProofContext.note_thmss ""
       (Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state))
         (no_binding args)))
   |> (fn (named_facts, state') =>
diff -r 0fffc66b10d7 -r ac7570d80c3d src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Mar 28 17:10:43 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sat Mar 28 17:21:11 2009 +0100
@@ -101,9 +101,7 @@
   val mandatory_path: string -> Proof.context -> Proof.context
   val restore_naming: Proof.context -> Proof.context -> Proof.context
   val reset_naming: Proof.context -> Proof.context
-  val note_thmss: string -> (Thm.binding * (Facts.ref * attribute list) list) list ->
-    Proof.context -> (string * thm list) list * Proof.context
-  val note_thmss_i: string -> (Thm.binding * (thm list * attribute list) list) list ->
+  val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
   val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
   val read_vars: (binding * string option * mixfix) list -> Proof.context ->
@@ -959,25 +957,23 @@
   | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
       (Facts.add_local do_props (naming_of ctxt) (b, ths) #> snd);
 
-fun gen_note_thmss get k = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
+in
+
+fun note_thmss kind = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
   let
     val pos = Binding.pos_of b;
     val name = full_name ctxt b;
     val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos;
 
-    val facts = PureThy.name_thmss false pos name (map (apfst (get ctxt)) raw_facts);
+    val facts = PureThy.name_thmss false pos name raw_facts;
     fun app (th, attrs) x =
-      swap (Library.foldl_map (Thm.proof_attributes (surround (Thm.kind k) (attrs @ more_attrs))) (x, th));
+      swap (Library.foldl_map
+        (Thm.proof_attributes (surround (Thm.kind kind) (attrs @ more_attrs))) (x, th));
     val (res, ctxt') = fold_map app facts ctxt;
     val thms = PureThy.name_thms false false pos name (flat res);
     val Mode {stmt, ...} = get_mode ctxt;
   in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);
 
-in
-
-fun note_thmss k = gen_note_thmss get_fact k;
-fun note_thmss_i k = gen_note_thmss (K I) k;
-
 fun put_thms do_props thms ctxt = ctxt
   |> map_naming (K local_naming)
   |> ContextPosition.set_visible false
@@ -1161,7 +1157,7 @@
   in
     ctxt2
     |> auto_bind_facts (flat propss)
-    |> note_thmss_i Thm.assumptionK (map fst args ~~ map (map (fn th => ([th], []))) premss)
+    |> note_thmss Thm.assumptionK (map fst args ~~ map (map (fn th => ([th], []))) premss)
   end;
 
 in
diff -r 0fffc66b10d7 -r ac7570d80c3d src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat Mar 28 17:10:43 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Sat Mar 28 17:21:11 2009 +0100
@@ -327,7 +327,7 @@
         val (facts, goal_ctxt) = elems_ctxt
           |> (snd o ProofContext.add_fixes_i [(Binding.name AutoBind.thesisN, NONE, NoSyn)])
           |> fold_map assume_case (obtains ~~ propp)
-          |-> (fn ths => ProofContext.note_thmss_i Thm.assumptionK
+          |-> (fn ths => ProofContext.note_thmss Thm.assumptionK
                 [((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
       in ((prems, stmt, facts), goal_ctxt) end);
 
@@ -370,7 +370,7 @@
       end;
   in
     goal_ctxt
-    |> ProofContext.note_thmss_i Thm.assumptionK
+    |> ProofContext.note_thmss Thm.assumptionK
       [((Binding.name AutoBind.assmsN, []), [(prems, [])])]
     |> snd
     |> Proof.theorem_i before_qed after_qed' (map snd stmt)
diff -r 0fffc66b10d7 -r ac7570d80c3d src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Sat Mar 28 17:10:43 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Sat Mar 28 17:21:11 2009 +0100
@@ -160,9 +160,9 @@
   in
     lthy |> LocalTheory.theory
       (PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd)
-    |> not is_locale ? LocalTheory.target (ProofContext.note_thmss_i kind global_facts #> snd)
+    |> not is_locale ? LocalTheory.target (ProofContext.note_thmss kind global_facts #> snd)
     |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
-    |> ProofContext.note_thmss_i kind local_facts
+    |> ProofContext.note_thmss kind local_facts
   end;
 
 
diff -r 0fffc66b10d7 -r ac7570d80c3d src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Sat Mar 28 17:10:43 2009 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Sat Mar 28 17:21:11 2009 +0100
@@ -87,7 +87,7 @@
 val _ = macro "note" (Args.context :|-- (fn ctxt =>
   P.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
     ((a, map (Attrib.attribute (ProofContext.theory_of ctxt)) srcs), [(ths, [])])))
-  >> (fn args => #2 (ProofContext.note_thmss_i "" args ctxt))));
+  >> (fn args => #2 (ProofContext.note_thmss "" args ctxt))));
 
 val _ = value "ctyp" (Args.typ >> (fn T =>
   "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)));