Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
qed: kind_name (again);
authorwenzelm
Tue, 01 Dec 1998 14:46:58 +0100
changeset 6001 28b0a9891852
parent 6000 aa84c30c1f61
child 6002 c1f28f8ec72c
qed: kind_name (again);
src/Pure/Isar/proof.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle