src/Pure/Isar/obtain.ML
changeset 18040 c67505cdecad
parent 17974 5b54db4a44ee
child 18124 a310c78298f9
     1.1 --- a/src/Pure/Isar/obtain.ML	Fri Oct 28 22:28:11 2005 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Fri Oct 28 22:28:12 2005 +0200
     1.3 @@ -57,10 +57,10 @@
     1.4      val cparms = map (Thm.cterm_of thy) parms;
     1.5  
     1.6      val thm' = thm
     1.7 -      |> Drule.implies_intr_goals cprops
     1.8 +      |> Drule.implies_intr_protected cprops
     1.9        |> Drule.forall_intr_list cparms
    1.10        |> Drule.forall_elim_vars (maxidx + 1);
    1.11 -    val elim_tacs = replicate (length cprops) (Tactic.etac Drule.goalI);
    1.12 +    val elim_tacs = replicate (length cprops) (Tactic.etac Drule.protectI);
    1.13  
    1.14      val concl = Logic.strip_assums_concl prop;
    1.15      val bads = parms inter (Term.term_frees concl);
    1.16 @@ -234,9 +234,7 @@
    1.17          #> Proof.add_binds_i AutoBind.no_facts
    1.18        end;
    1.19  
    1.20 -    val before_qed = SOME (Method.primitive_text (fn th =>
    1.21 -      let val th' = Goal.conclude th
    1.22 -      in th' COMP Drule.incr_indexes_wrt [] [] [] [th'] Drule.goalI end));
    1.23 +    val before_qed = SOME (Method.primitive_text (Goal.conclude #> Goal.protect));
    1.24      fun after_qed _ [[res]] =
    1.25        (check_result res; Proof.end_block #> Seq.map (`Proof.the_fact #-> guess_context));
    1.26    in