# HG changeset patch # User wenzelm # Date 1238256643 -3600 # Node ID 0fffc66b10d72a9603d38d68fd216b62039ae7aa # Parent 3bc78fbb9f57f5b3cfb8c6a951ccf4523ffb7e11 simplified references to facts, eliminated external note_thmss; diff -r 3bc78fbb9f57 -r 0fffc66b10d7 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;