src/Pure/Isar/proof.ML
changeset 12808 a529b4b91888
parent 12760 2356740225ce
child 12930 c1f3ff5feff1
     1.1 --- a/src/Pure/Isar/proof.ML	Thu Jan 17 21:05:58 2002 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu Jan 17 21:06:23 2002 +0100
     1.3 @@ -479,11 +479,10 @@
     1.4      val th = raw_th RS Drule.rev_triv_goal;
     1.5      val ths = Drule.conj_elim_precise (length ts) th
     1.6        handle THM _ => err "Main goal structure corrupted";
     1.7 -    val props = map (#prop o Thm.rep_thm) ths;
     1.8    in
     1.9      conditional (not (null bad_hyps)) (fn () => err ("Additional hypotheses:\n" ^
    1.10          cat_lines (map (ProofContext.string_of_term ctxt) bad_hyps)));
    1.11 -    conditional (exists (not o Pattern.matches tsig) (ts ~~ props)) (fn () =>
    1.12 +    conditional (exists (not o Pattern.matches tsig) (ts ~~ map Thm.prop_of ths)) (fn () =>
    1.13        err ("Proved a different theorem: " ^ Pretty.string_of (ProofContext.pretty_thm ctxt th)));
    1.14      ths
    1.15    end;
    1.16 @@ -641,9 +640,10 @@
    1.17        |> enter_forward
    1.18        |> opt_block
    1.19        |> map_context_result (fn ctxt => prepp (ctxt, raw_propp));
    1.20 +    val sign' = sign_of state';
    1.21  
    1.22      val props = flat propss;
    1.23 -    val cprop = Thm.cterm_of (sign_of state') (Logic.mk_conjunction_list props);
    1.24 +    val cprop = Thm.cterm_of sign' (Logic.mk_conjunction_list props);
    1.25      val goal = Drule.mk_triv_goal cprop;
    1.26  
    1.27      val tvars = foldr Term.add_term_tvars (props, []);
    1.28 @@ -659,7 +659,8 @@
    1.29      |> map_context (autofix props)
    1.30      |> put_goal (Some (((kind, names, propss), ([], goal)), after_qed o map_context gen_binds))
    1.31      |> map_context (ProofContext.add_cases
    1.32 -     (if length props = 1 then RuleCases.make true goal [rule_contextN]
    1.33 +     (if length props = 1 then
    1.34 +      RuleCases.make true (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN]
    1.35        else [(rule_contextN, RuleCases.empty)]))
    1.36      |> auto_bind_goal props
    1.37      |> (if is_chain state then use_facts else reset_facts)