# HG changeset patch
# User wenzelm
# Date 928184953 -7200
# Node ID 0545b77f864e9206f257c2633c9d520abdd2fc22
# Parent  0e346c73828c834fe24e20126b45788dcb303488
setup_goal: proper handling of non-atomic goals (include cprems into asms);

diff -r 0e346c73828c -r 0545b77f864e src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon May 31 19:08:26 1999 +0200
+++ b/src/Pure/Isar/proof.ML	Mon May 31 23:09:13 1999 +0200
@@ -489,16 +489,16 @@
       |> enter_forward
       |> opt_block
       |> map_context_result (fn c => prepp (c, raw_propp));
+    val cterm_of = Thm.cterm_of (sign_of state);
 
     val casms = map (#prop o Thm.crep_thm) (ProofContext.assumptions (context_of state'));
-    val asms = map Thm.term_of casms;
-
-    val prop = Logic.list_implies (asms, concl);
-    val cprop = Thm.cterm_of (sign_of state') prop;
+    val cprems = map cterm_of (Logic.strip_imp_prems concl);
+    val prop = Logic.list_implies (map Thm.term_of casms, concl);
+    val cprop = cterm_of prop;
     val thm = Drule.mk_triv_goal cprop;
   in
     state'
-    |> put_goal (Some ((kind atts, (PureThy.default_name name), casms, prop), ([], thm)))
+    |> put_goal (Some ((kind atts, (PureThy.default_name name), casms @ cprems, prop), ([], thm)))
     |> bind_props [("thesis", prop)]
     |> (if is_chain state then use_facts else reset_facts)
     |> new_block