# HG changeset patch
# User wenzelm
# Date 912342049 -3600
# Node ID d03fbef54c62c58db996149d97502a751c4eb39a
# Parent  263051aaf0deeffe256c9b20f29e4d4ddc3f4c56
tuned print_state;
changed solve semantics: support back-pressure of asms (cut, def etc.);

diff -r 263051aaf0de -r d03fbef54c62 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun Nov 29 13:19:48 1998 +0100
+++ b/src/Pure/Isar/proof.ML	Sun Nov 29 13:20:49 1998 +0100
@@ -282,12 +282,12 @@
   in
     writeln ("Nesting level: " ^ string_of_int (length nodes div 1));	(* FIXME *)
     writeln "";
+    writeln (mode_name mode ^ " mode");
+    writeln "";
     ProofContext.print_context context;
     writeln "";
     print_facts facts;
-    print_goal (find_goal 0 state);
-    writeln "";
-    writeln (mode_name mode ^ " mode")
+    print_goal (find_goal 0 state)
   end;
 
 
@@ -406,7 +406,7 @@
 fun solve_goal rule state =
   let
     val (_, (result, (facts, thm))) = find_goal 0 state;
-    val thms' = FIRSTGOAL (solve_tac [rule]) thm;
+    val thms' = FIRSTGOAL (rtac rule THEN_ALL_NEW (TRY o assume_tac)) thm;
   in Seq.map (fn thm' => map_goal (K (result, (facts, thm'))) state) thms' end;