src/Pure/Isar/proof.ML
changeset 6752 0545b77f864e
parent 6731 57e761134c85
child 6756 fe6eb161df3e
     1.1 --- a/src/Pure/Isar/proof.ML	Mon May 31 19:08:26 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Mon May 31 23:09:13 1999 +0200
     1.3 @@ -489,16 +489,16 @@
     1.4        |> enter_forward
     1.5        |> opt_block
     1.6        |> map_context_result (fn c => prepp (c, raw_propp));
     1.7 +    val cterm_of = Thm.cterm_of (sign_of state);
     1.8  
     1.9      val casms = map (#prop o Thm.crep_thm) (ProofContext.assumptions (context_of state'));
    1.10 -    val asms = map Thm.term_of casms;
    1.11 -
    1.12 -    val prop = Logic.list_implies (asms, concl);
    1.13 -    val cprop = Thm.cterm_of (sign_of state') prop;
    1.14 +    val cprems = map cterm_of (Logic.strip_imp_prems concl);
    1.15 +    val prop = Logic.list_implies (map Thm.term_of casms, concl);
    1.16 +    val cprop = cterm_of prop;
    1.17      val thm = Drule.mk_triv_goal cprop;
    1.18    in
    1.19      state'
    1.20 -    |> put_goal (Some ((kind atts, (PureThy.default_name name), casms, prop), ([], thm)))
    1.21 +    |> put_goal (Some ((kind atts, (PureThy.default_name name), casms @ cprems, prop), ([], thm)))
    1.22      |> bind_props [("thesis", prop)]
    1.23      |> (if is_chain state then use_facts else reset_facts)
    1.24      |> new_block