# HG changeset patch
# User wenzelm
# Date 1164128860 -3600
# Node ID 56e54a2afe695cd2a3448a13f1d8b8e2178a8ff9
# Parent  940ef3e85c5a77d2cba85e2ed8ef31e5c38e107f
simplified theorem(_i);
notes: proper kind;
renamed put_thms_internal to put_thms;

diff -r 940ef3e85c5a -r 56e54a2afe69 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Nov 21 18:07:38 2006 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Nov 21 18:07:40 2006 +0100
@@ -18,8 +18,7 @@
   val theory_of: state -> theory
   val map_context: (context -> context) -> state -> state
   val add_binds_i: (indexname * term option) list -> state -> state
-  val put_thms: bool -> string * thm list option -> state -> state
-  val put_thms_internal: string * thm list option -> state -> state
+  val put_thms: string * thm list option -> state -> state
   val the_facts: state -> thm list
   val the_fact: state -> thm
   val put_facts: thm list option -> state -> state
@@ -90,9 +89,9 @@
     string -> Method.text option -> (thm list list -> state -> state Seq.seq) ->
     ((string * 'a list) * 'b) list -> state -> state
   val local_qed: Method.text option * bool -> state -> state Seq.seq
-  val theorem: string -> Method.text option -> (thm list list -> context -> context) ->
+  val theorem: Method.text option -> (thm list list -> context -> context) ->
     (string * string list) list list -> context -> state
-  val theorem_i: string -> Method.text option -> (thm list list -> context -> context) ->
+  val theorem_i: Method.text option -> (thm list list -> context -> context) ->
     (term * term list) list list -> context -> state
   val global_qed: Method.text option * bool -> state -> context
   val local_terminal_proof: Method.text * Method.text option -> state -> state Seq.seq
@@ -194,8 +193,7 @@
   f (context_of state) ||> (fn ctxt => map_context (K ctxt) state);
 
 val add_binds_i = map_context o ProofContext.add_binds_i;
-val put_thms = map_context oo ProofContext.put_thms;
-val put_thms_internal = map_context o ProofContext.put_thms_internal;
+val put_thms = map_context o ProofContext.put_thms;
 
 
 (* facts *)
@@ -212,7 +210,7 @@
 
 fun put_facts facts =
   map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
-  put_thms_internal (AutoBind.thisN, facts);
+  put_thms (AutoBind.thisN, facts);
 
 fun these_factss more_facts (named_factss, state) =
   (named_factss, state |> put_facts (SOME (maps snd named_factss @ more_facts)));
@@ -334,11 +332,11 @@
       (case filter_out (equal "") strs of [] => ""
       | strs' => enclose " (" ")" (commas strs'));
 
-    fun prt_goal (SOME (ctxt, (i, {statement = (kind, _), using, goal, before_qed, after_qed}))) =
+    fun prt_goal (SOME (ctxt, (i, {using, goal, before_qed, after_qed, ...}))) =
           pretty_facts "using " ctxt
             (if mode <> Backward orelse null using then NONE else SOME using) @
-          [Pretty.str ("goal" ^ description [kind, levels_up (i div 2),
-              subgoals (Thm.nprems_of goal)] ^ ":")] @
+          [Pretty.str ("goal" ^
+            description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @
           pretty_goals_local ctxt bg (true, ! show_main_goal) (! Display.goals_limit) goal
       | prt_goal NONE = [];
 
@@ -597,19 +595,19 @@
 
 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 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;
+  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 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;
+  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 local_results =
-  gen_thmss ProofContext.note_thmss_i (K []) I I (K I) o map (apsnd Thm.simple_fact);
+  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, [])])];
@@ -624,7 +622,8 @@
 fun gen_using f g note prep_atts args state =
   state
   |> assert_backward
-  |> map_context_result (note (Attrib.map_facts (prep_atts (theory_of state)) (no_binding args)))
+  |> map_context_result
+    (note "" (Attrib.map_facts (prep_atts (theory_of state)) (no_binding args)))
   |> (fn (named_facts, state') =>
     state' |> map_goal I (fn (statement, using, goal, before_qed, after_qed) =>
       let
@@ -834,9 +833,9 @@
 
 (* global goals *)
 
-fun global_goal prepp kind before_qed after_qed propp ctxt =
+fun global_goal prepp before_qed after_qed propp ctxt =
   init ctxt
-  |> generic_goal (prepp #> ProofContext.auto_fixes) kind
+  |> generic_goal (prepp #> ProofContext.auto_fixes) ""
     before_qed (K Seq.single, after_qed) propp;
 
 val theorem = global_goal ProofContext.bind_propp_schematic;