src/Pure/Isar/proof.ML
changeset 6001 28b0a9891852
parent 5993 d03fbef54c62
child 6030 f29d4e507564
--- 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