src/Pure/Isar/isar_thy.ML
changeset 7572 6e6dafacbc28
parent 7506 08a88d4ebd54
child 7590 76c9e71d491a
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Tue Sep 21 23:06:50 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Wed Sep 22 20:57:51 1999 +0200
     1.3 @@ -225,7 +225,11 @@
     1.4    f name (map (attrib x) more_srcs)
     1.5      (map (fn (s, srcs) => (get x s, map (attrib x) srcs)) th_srcs) x;
     1.6  
     1.7 -fun global_have_thmss x = gen_have_thmss PureThy.get_thms Attrib.global_attribute x;
     1.8 +fun global_have_thmss kind f (x as ((name, _), _)) thy =
     1.9 +  let val (thy', thms) = gen_have_thmss PureThy.get_thms Attrib.global_attribute f x thy in
    1.10 +    if kind <> "" then Context.setmp (Some thy') (Present.results kind name) thms else ();
    1.11 +    (thy', thms)
    1.12 +  end;
    1.13  
    1.14  fun local_have_thmss x =
    1.15    gen_have_thmss (ProofContext.get_thms o Proof.context_of)
    1.16 @@ -237,11 +241,11 @@
    1.17  fun have_lemss name atts = PureThy.have_thmss name (atts @ [Drule.tag_lemma]);
    1.18  
    1.19  
    1.20 -fun apply_theorems th_srcs = global_have_thmss PureThy.have_thmss (("", []), th_srcs);
    1.21 +fun apply_theorems th_srcs = global_have_thmss "" PureThy.have_thmss (("", []), th_srcs);
    1.22  fun apply_theorems_i th_srcs = gen_have_thmss_i PureThy.have_thmss (("", []), th_srcs);
    1.23 -val have_theorems = #1 oo (global_have_thmss PureThy.have_thmss o Comment.ignore);
    1.24 +val have_theorems = #1 oo (global_have_thmss "theorems" PureThy.have_thmss o Comment.ignore);
    1.25  val have_theorems_i = #1 oo (gen_have_thmss_i PureThy.have_thmss o Comment.ignore);
    1.26 -val have_lemmas = #1 oo (global_have_thmss have_lemss o Comment.ignore);
    1.27 +val have_lemmas = #1 oo (global_have_thmss "lemmas" have_lemss o Comment.ignore);
    1.28  val have_lemmas_i = #1 oo (gen_have_thmss_i have_lemss o Comment.ignore);
    1.29  val have_facts = ProofHistory.apply o local_have_thmss (Proof.have_thmss []) o Comment.ignore;
    1.30  val have_facts_i = ProofHistory.apply o gen_have_thmss_i (Proof.have_thmss []) o Comment.ignore;
    1.31 @@ -335,12 +339,17 @@
    1.32  
    1.33  (* print result *)
    1.34  
    1.35 +local
    1.36 +
    1.37  fun pretty_result {kind, name, thm} =
    1.38 -  Pretty.block [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Proof.pretty_thm thm];
    1.39 +  Pretty.block [Pretty.str (kind ^ (if name = "" then "" else " " ^ name ^ ":")),
    1.40 +    Pretty.fbrk, Proof.pretty_thm thm];
    1.41  
    1.42  fun pretty_rule thm =
    1.43    Pretty.block [Pretty.str "trying to solve goal by rule:", Pretty.fbrk, Proof.pretty_thm thm];
    1.44  
    1.45 +in
    1.46 +
    1.47  val print_result = Pretty.writeln o pretty_result;
    1.48  
    1.49  fun cond_print_result_rule int =
    1.50 @@ -349,6 +358,8 @@
    1.51  
    1.52  fun proof'' f = Toplevel.proof' (f o cond_print_result_rule);
    1.53  
    1.54 +end;
    1.55 +
    1.56  
    1.57  (* local endings *)
    1.58  
    1.59 @@ -373,8 +384,8 @@
    1.60    let
    1.61      val state = ProofHistory.current prf;
    1.62      val _ = if Proof.at_bottom state then () else raise Toplevel.UNDEF;
    1.63 -    val (thy, res) = finish state;
    1.64 -  in print_result res; thy end);
    1.65 +    val (thy, res as {kind, name, thm}) = finish state;
    1.66 +  in print_result res; Context.setmp (Some thy) (Present.result kind name) thm; thy end);
    1.67  
    1.68  val global_qed = global_result o Method.global_qed o apsome Comment.ignore_interest;
    1.69  val global_terminal_proof = global_result o Method.global_terminal_proof o ignore_interests;