# HG changeset patch
# User wenzelm
# Date 1125237890 -7200
# Node ID dc3b8cec8bba2d234d874d247245bb6edce6b6ee
# Parent  9b498019723f8606ce48e0e86effe67960c6898a
tuned;

diff -r 9b498019723f -r dc3b8cec8bba NEWS
--- a/NEWS	Sun Aug 28 16:04:49 2005 +0200
+++ b/NEWS	Sun Aug 28 16:04:50 2005 +0200
@@ -19,7 +19,7 @@
 
 will disappear in the next release.  Use isatool fixheaders to convert
 existing theory files.  Note that there is no change in ancient
-non-Isar theories.
+non-Isar theories now, but these are likely to disappear soon.
 
 * Theory loader: parent theories can now also be referred to via
 relative and absolute paths.
@@ -659,6 +659,11 @@
 provides a clean interface for unusual systems where the internal and
 external process view of file names are different.
 
+* ML functions legacy_bindings and use_legacy_bindings produce ML fact
+bindings for all theorems stored within a given theory; this may help
+in porting non-Isar theories to Isar ones, while keeping ML proof
+scripts for the time being.
+
 
 *** System ***
 
diff -r 9b498019723f -r dc3b8cec8bba src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun Aug 28 16:04:49 2005 +0200
+++ b/src/Pure/Isar/proof.ML	Sun Aug 28 16:04:50 2005 +0200
@@ -623,7 +623,7 @@
 
 (* note / from / with *)
 
-fun no_result args = map (pair ("", [])) args;
+fun no_binding args = map (pair ("", [])) args;
 
 local
 
@@ -641,12 +641,12 @@
 fun simple_note_thms name thms = note_thmss_i [((name, []), [(thms, [])])];
 
 val from_thmss =
-  gen_thmss ProofContext.note_thmss (K []) chain Attrib.local_attribute o no_result;
-val from_thmss_i = gen_thmss ProofContext.note_thmss_i (K []) chain (K I) o no_result;
+  gen_thmss ProofContext.note_thmss (K []) chain Attrib.local_attribute o no_binding;
+val from_thmss_i = gen_thmss ProofContext.note_thmss_i (K []) chain (K I) o no_binding;
 
 val with_thmss =
-  gen_thmss ProofContext.note_thmss the_facts chain Attrib.local_attribute o no_result;
-val with_thmss_i = gen_thmss ProofContext.note_thmss_i the_facts chain (K I) o no_result;
+  gen_thmss ProofContext.note_thmss the_facts chain Attrib.local_attribute o no_binding;
+val with_thmss_i = gen_thmss ProofContext.note_thmss_i the_facts chain (K I) o no_binding;
 
 end;
 
@@ -658,7 +658,7 @@
 fun gen_using_thmss note prep_atts args state =
   state
   |> assert_backward
-  |> map_context_result (note (Attrib.map_facts (prep_atts (theory_of state)) (no_result args)))
+  |> map_context_result (note (Attrib.map_facts (prep_atts (theory_of state)) (no_binding args)))
   |> (fn (st, named_facts) =>
     let val (_, (_, ((result, (facts, thm)), x))) = find_goal st;
     in st |> map_goal I (K ((result, (facts @ List.concat (map snd named_facts), thm)), x)) end);
@@ -957,14 +957,8 @@
 fun defer i = assert_no_chain #> refine (Method.Basic (K (Method.defer i)));
 fun prefer i = assert_no_chain #> refine (Method.Basic (K (Method.prefer i)));
 
-fun apply text =
-  assert_backward
-  #> refine text
-  #> Seq.map (goal_facts (K []));
-
-fun apply_end text =
-  assert_forward
-  #> refine_end text;
+fun apply text = assert_backward #> refine text #> Seq.map (goal_facts (K []));
+fun apply_end text = assert_forward #> refine_end text;