# HG changeset patch
# User wenzelm
# Date 912520018 -3600
# Node ID 28b0a98918525d0678c890d80ede4f51c7aaf78f
# Parent  aa84c30c1f610cb746c929873dbbc720dc03f22b
qed: kind_name (again);

diff -r aa84c30c1f61 -r 28b0a9891852 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Dec 01 14:46:35 1998 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Dec 01 14:46:58 1998 +0100
@@ -83,9 +83,8 @@
   Goal of context attribute list |      (*intermediate result, solving subgoal*)
   Aux of context attribute list ;       (*intermediate result*)
 
-val theoremN = "theorem";
 val kind_name =
-  fn Theorem _ => theoremN | Lemma _ => "lemma" | Goal _ => "show" | Aux _ => "have";
+  fn Theorem _ => "theorem" | Lemma _ => "lemma" | Goal _ => "show" | Aux _ => "have";
 
 type goal =
  (kind *		(*result kind*)
@@ -631,7 +630,7 @@
       | _ => raise STATE ("No global goal!", state));
 
     val (thy', result') = PureThy.store_tthm ((name, (result, [])), atts) (theory_of state);
-  in (thy', (theoremN, name, result')) end;
+  in (thy', (kind_name kind, name, result')) end;
 
 fun qed meth_fun alt_name alt_atts state =
   state