# 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