# HG changeset patch
# User wenzelm
# Date 1164138486 -3600
# Node ID 0413b46ee5efae8e9845ebd183277de4ab10b4fe
# Parent  09c953c07008b07c3ef1de1c0b2e95f6dd7d5097
removed obsolete simple_note_thms;

diff -r 09c953c07008 -r 0413b46ee5ef src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Nov 21 20:48:03 2006 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Nov 21 20:48:06 2006 +0100
@@ -60,7 +60,6 @@
   val chain: state -> state
   val chain_facts: thm list -> state -> state
   val get_thmss: state -> (thmref * Attrib.src list) list -> thm list
-  val simple_note_thms: string -> thm list -> state -> state
   val note_thmss: ((string * Attrib.src list) *
     (thmref * Attrib.src list) list) list -> state -> state
   val note_thmss_i: ((string * attribute list) *
@@ -610,7 +609,6 @@
   gen_thmss (ProofContext.note_thmss_i "") (K []) I I (K I) o map (apsnd Thm.simple_fact);
 
 fun get_thmss state srcs = the_facts (note_thmss [(("", []), srcs)] state);
-fun simple_note_thms name thms = note_thmss_i [((name, []), [(thms, [])])];
 
 end;
 
@@ -661,7 +659,7 @@
     |> assume_i assumptions
     |> add_binds_i AutoBind.no_facts
     |> map_context (ProofContext.restore_naming (context_of state))
-    |> `the_facts |-> simple_note_thms name
+    |> `the_facts |-> (fn thms => note_thmss_i [((name, []), [(thms, [])])])
   end;
 
 in