1.1 --- a/src/Pure/Isar/obtain.ML	Tue Oct 16 23:00:21 2001 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Tue Oct 16 23:02:14 2001 +0200
     1.3 @@ -32,18 +32,18 @@
     1.4  struct
     1.5  
     1.6  
     1.7 -(** disch_obtained **)
     1.8 +(** export_obtain **)
     1.9  
    1.10 -fun disch_obtained state parms rule cprops thm =
    1.11 +fun export_obtain state parms rule _ cprops thm =
    1.12    let
    1.13      val {sign, prop, maxidx, ...} = Thm.rep_thm thm;
    1.14      val cparms = map (Thm.cterm_of sign) parms;
    1.15  
    1.16      val thm' = thm
    1.17 -      |> Drule.implies_intr_list cprops
    1.18 +      |> Drule.implies_intr_goals cprops
    1.19        |> Drule.forall_intr_list cparms
    1.20        |> Drule.forall_elim_vars (maxidx + 1);
    1.21 -    val elim_tacs = replicate (length cprops) Proof.hard_asm_tac;
    1.22 +    val elim_tacs = replicate (length cprops) (Tactic.etac Drule.triv_goal);
    1.23  
    1.24      val concl = Logic.strip_assums_concl prop;
    1.25      val bads = parms inter (Term.term_frees concl);
    1.26 @@ -100,14 +100,11 @@
    1.27        Term.list_all_free (map #1 parm_names, Logic.list_implies (asm_props, bound_thesis))
    1.28        |> Library.curry Logic.list_rename_params (map #2 parm_names);
    1.29  
    1.30 -    fun export_obtained rule =
    1.31 -      (disch_obtained state parms rule, fn _ => fn _ => []);
    1.32 -
    1.33      fun after_qed st = st
    1.34        |> Proof.end_block
    1.35        |> Seq.map (fn st' => st'
    1.36          |> Proof.fix_i vars
    1.37 -        |> Proof.assm_i (export_obtained (Proof.the_fact st')) asms);
    1.38 +        |> Proof.assm_i (export_obtain state parms (Proof.the_fact st')) asms);
    1.39    in
    1.40      state
    1.41      |> Proof.enter_forward