qed: kind_name (again);
authorwenzelm
Tue Dec 01 14:46:58 1998 +0100 (1998-12-01)
changeset 600128b0a9891852
parent 6000 aa84c30c1f61
child 6002 c1f28f8ec72c
qed: kind_name (again);
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Tue Dec 01 14:46:35 1998 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Tue Dec 01 14:46:58 1998 +0100
     1.3 @@ -83,9 +83,8 @@
     1.4    Goal of context attribute list |      (*intermediate result, solving subgoal*)
     1.5    Aux of context attribute list ;       (*intermediate result*)
     1.6  
     1.7 -val theoremN = "theorem";
     1.8  val kind_name =
     1.9 -  fn Theorem _ => theoremN | Lemma _ => "lemma" | Goal _ => "show" | Aux _ => "have";
    1.10 +  fn Theorem _ => "theorem" | Lemma _ => "lemma" | Goal _ => "show" | Aux _ => "have";
    1.11  
    1.12  type goal =
    1.13   (kind *		(*result kind*)
    1.14 @@ -631,7 +630,7 @@
    1.15        | _ => raise STATE ("No global goal!", state));
    1.16  
    1.17      val (thy', result') = PureThy.store_tthm ((name, (result, [])), atts) (theory_of state);
    1.18 -  in (thy', (theoremN, name, result')) end;
    1.19 +  in (thy', (kind_name kind, name, result')) end;
    1.20  
    1.21  fun qed meth_fun alt_name alt_atts state =
    1.22    state