src/Pure/Isar/proof.ML
changeset 6996 1a28d968c5aa
parent 6982 4d2a3f35af93
child 7011 7e8e9a26ba2c
     1.1 --- a/src/Pure/Isar/proof.ML	Tue Jul 13 13:53:34 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Tue Jul 13 13:54:08 1999 +0200
     1.3 @@ -388,7 +388,7 @@
     1.4  fun export_wrt inner opt_outer =
     1.5    let
     1.6      val (fixes, asms) = diff_context inner opt_outer;
     1.7 -    val casms = map #1 asms;
     1.8 +    val casms = map (Drule.mk_cgoal o #1) asms;
     1.9      val tacs = map #2 asms;
    1.10    in (export fixes casms, tacs) end;
    1.11  
    1.12 @@ -449,7 +449,7 @@
    1.13      val tsig = Sign.tsig_of sign;
    1.14  
    1.15      val casms = map #1 (assumptions state);
    1.16 -    val bad_hyps = Library.gen_rems Term.aconv (hyps, map Thm.term_of casms);
    1.17 +    val bad_hyps = Library.gen_rems Term.aconv (hyps, map (Thm.term_of o Drule.mk_cgoal) casms);
    1.18    in
    1.19      if not (null bad_hyps) then
    1.20        err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) bad_hyps))
    1.21 @@ -538,10 +538,13 @@
    1.22  val assm = gen_assume ProofContext.assume;
    1.23  val assm_i = gen_assume ProofContext.assume_i;
    1.24  
    1.25 -val assume = assm (assume_tac, K all_tac);
    1.26 -val assume_i = assm_i (assume_tac, K all_tac);
    1.27 -val presume = assm (K all_tac, K all_tac);
    1.28 -val presume_i = assm_i (K all_tac, K all_tac);
    1.29 +val hard_asm_tac = Tactic.etac Drule.triv_goal;
    1.30 +val soft_asm_tac = Tactic.rtac Drule.triv_goal;
    1.31 +
    1.32 +val assume = assm (hard_asm_tac, soft_asm_tac);
    1.33 +val assume_i = assm_i (hard_asm_tac, soft_asm_tac);
    1.34 +val presume = assm (soft_asm_tac, soft_asm_tac);
    1.35 +val presume_i = assm_i (soft_asm_tac, soft_asm_tac);
    1.36  
    1.37  
    1.38  
    1.39 @@ -581,7 +584,7 @@
    1.40      val casms = map #1 (assumptions state');
    1.41  
    1.42      val revcut_rl = Drule.incr_indexes_wrt [] [] (cprop :: casms) [] Drule.revcut_rl;
    1.43 -    fun cut_asm (casm, thm) = Thm.rotate_rule ~1 1 ((Thm.assume casm COMP revcut_rl) RS thm);
    1.44 +    fun cut_asm (casm, thm) = Thm.rotate_rule ~1 1 ((Drule.assume_goal casm COMP revcut_rl) RS thm);
    1.45      val goal = foldr cut_asm (casms, Drule.mk_triv_goal cprop);
    1.46    in
    1.47      state'