src/Pure/Isar/proof.ML

--- a/src/Pure/Isar/proof.ML	Sat Mar 28 17:08:49 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Sat Mar 28 17:10:43 2009 +0100
@@ -620,29 +620,27 @@
 
 local
 
-fun gen_thmss note_ctxt more_facts opt_chain opt_result prep_atts args state =
+fun gen_thmss more_facts opt_chain opt_result prep_atts prep_fact args state =
   state
   |> assert_forward
-  |> map_context_result (note_ctxt (Attrib.map_facts (prep_atts (theory_of state)) args))
+  |> map_context_result (ProofContext.note_thmss_i ""
+    (Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state)) args))
   |> these_factss (more_facts state)
   ||> opt_chain
   |> opt_result;
 
 in
 
-val note_thmss = gen_thmss (ProofContext.note_thmss "") (K []) I #2 Attrib.attribute;
-val note_thmss_i = gen_thmss (ProofContext.note_thmss_i "") (K []) I #2 (K I);
-
-val from_thmss =
-  gen_thmss (ProofContext.note_thmss "") (K []) chain #2 Attrib.attribute o no_binding;
-val from_thmss_i = gen_thmss (ProofContext.note_thmss_i "") (K []) chain #2 (K I) o no_binding;
+val note_thmss = gen_thmss (K []) I #2 Attrib.attribute ProofContext.get_fact;
+val note_thmss_i = gen_thmss (K []) I #2 (K I) (K I);
 
-val with_thmss =
-  gen_thmss (ProofContext.note_thmss "") the_facts chain #2 Attrib.attribute o no_binding;
-val with_thmss_i = gen_thmss (ProofContext.note_thmss_i "") the_facts chain #2 (K I) o no_binding;
+val from_thmss = gen_thmss (K []) chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
+val from_thmss_i = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
 
-val local_results =
-  gen_thmss (ProofContext.note_thmss_i "") (K []) I I (K I) o map (apsnd Thm.simple_fact);
+val with_thmss = gen_thmss the_facts chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
+val with_thmss_i = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
+
+val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
 
 fun get_thmss state srcs = the_facts (note_thmss [((Binding.empty, []), srcs)] state);
 
@@ -653,11 +651,13 @@
 
 local
 
-fun gen_using f g note prep_atts args state =
+fun gen_using f g prep_atts prep_fact args state =
   state
   |> assert_backward
   |> map_context_result
-    (note "" (Attrib.map_facts (prep_atts (theory_of state)) (no_binding args)))
+    (ProofContext.note_thmss_i ""
+      (Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state))
+        (no_binding args)))
   |> (fn (named_facts, state') =>
     state' |> map_goal I (fn (statement, _, using, goal, before_qed, after_qed) =>
       let
@@ -671,10 +671,10 @@
 
 in
 
-val using = gen_using append_using (K (K I)) ProofContext.note_thmss Attrib.attribute;
-val using_i = gen_using append_using (K (K I)) ProofContext.note_thmss_i (K I);
-val unfolding = gen_using unfold_using unfold_goals ProofContext.note_thmss Attrib.attribute;
-val unfolding_i = gen_using unfold_using unfold_goals ProofContext.note_thmss_i (K I);
+val using = gen_using append_using (K (K I)) Attrib.attribute ProofContext.get_fact;
+val using_i = gen_using append_using (K (K I)) (K I) (K I);
+val unfolding = gen_using unfold_using unfold_goals Attrib.attribute ProofContext.get_fact;
+val unfolding_i = gen_using unfold_using unfold_goals (K I) (K I);
 
 end;