simplified exporter interface;

--- a/src/Pure/Isar/local_defs.ML	Tue Oct 16 23:00:21 2001 +0200
+++ b/src/Pure/Isar/local_defs.ML	Tue Oct 16 23:02:14 2001 +0200
@@ -18,30 +18,20 @@
 struct
 
 
-(* export_defs *)
-
-local
-
-val refl_tac = Tactic.rtac (Drule.reflexive_thm RS Drule.triv_goal);
+(* export_def *)
 
 fun dest_lhs cprop =
-  let val x = #1 (Logic.dest_equals (Logic.dest_goal (Thm.term_of cprop)))
+  let val x = #1 (Logic.dest_equals (Thm.term_of cprop))
   in Term.dest_Free x; Thm.cterm_of (Thm.sign_of_cterm cprop) x end
   handle TERM _ => raise TERM ("Malformed definitional assumption encountered:\n" ^
       quote (Display.string_of_cterm cprop), []);
 
-fun disch_defs cprops thm =
+fun export_def _ cprops thm =
   thm
   |> Drule.implies_intr_list cprops
   |> Drule.forall_intr_list (map dest_lhs cprops)
   |> Drule.forall_elim_vars 0
-  |> RANGE (replicate (length cprops) refl_tac) 1;
-
-in
-
-val export_defs = (disch_defs, fn _ => fn _ => []);
-
-end;
+  |> RANGE (replicate (length cprops) (Tactic.rtac Drule.reflexive_thm)) 1;
 
 
 (* def(_i) *)
@@ -63,7 +53,7 @@
     state
     |> fix [([x], None)]
     |> Proof.match_bind_i [(pats, rhs)]
-    |> Proof.assm_i export_defs [((name, atts), [(Logic.mk_equals (lhs, rhs), ([], []))])]
+    |> Proof.assm_i export_def [((name, atts), [(Logic.mk_equals (lhs, rhs), ([], []))])]
   end;
 
 val def = gen_def Proof.fix ProofContext.read_term ProofContext.read_term_pats;

--- a/src/Pure/Isar/obtain.ML	Tue Oct 16 23:00:21 2001 +0200
+++ b/src/Pure/Isar/obtain.ML	Tue Oct 16 23:02:14 2001 +0200
@@ -32,18 +32,18 @@
 struct
 
 
-(** disch_obtained **)
+(** export_obtain **)
 
-fun disch_obtained state parms rule cprops thm =
+fun export_obtain state parms rule _ cprops thm =
   let
     val {sign, prop, maxidx, ...} = Thm.rep_thm thm;
     val cparms = map (Thm.cterm_of sign) parms;
 
     val thm' = thm
-      |> Drule.implies_intr_list cprops
+      |> Drule.implies_intr_goals cprops
       |> Drule.forall_intr_list cparms
       |> Drule.forall_elim_vars (maxidx + 1);
-    val elim_tacs = replicate (length cprops) Proof.hard_asm_tac;
+    val elim_tacs = replicate (length cprops) (Tactic.etac Drule.triv_goal);
 
     val concl = Logic.strip_assums_concl prop;
     val bads = parms inter (Term.term_frees concl);
@@ -100,14 +100,11 @@
       Term.list_all_free (map #1 parm_names, Logic.list_implies (asm_props, bound_thesis))
       |> Library.curry Logic.list_rename_params (map #2 parm_names);
 
-    fun export_obtained rule =
-      (disch_obtained state parms rule, fn _ => fn _ => []);
-
     fun after_qed st = st
       |> Proof.end_block
       |> Seq.map (fn st' => st'
         |> Proof.fix_i vars
-        |> Proof.assm_i (export_obtained (Proof.the_fact st')) asms);
+        |> Proof.assm_i (export_obtain state parms (Proof.the_fact st')) asms);
   in
     state
     |> Proof.enter_forward

--- a/src/Pure/Isar/proof.ML	Tue Oct 16 23:00:21 2001 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Oct 16 23:02:14 2001 +0200
@@ -62,8 +62,6 @@
     (thm list * context attribute list) list) list -> state -> state
   val fix: (string list * string option) list -> state -> state
   val fix_i: (string list * typ option) list -> state -> state
-  val hard_asm_tac: int -> tactic
-  val soft_asm_tac: int -> tactic
   val assm: ProofContext.exporter
     -> ((string * context attribute list) * (string * (string list * string list)) list) list
     -> state -> state
@@ -413,20 +411,26 @@
 
 (* export results *)
 
+fun refine_tac rule =
+  Tactic.rtac rule THEN_ALL_NEW (SUBGOAL (fn (goal, i) =>
+    if can Logic.dest_goal (Logic.strip_assums_concl goal) then
+      Tactic.etac Drule.triv_goal i
+    else all_tac));
+
 fun export_goal print_rule raw_rule inner state =
   let
     val (outer, (_, ((result, (facts, thm)), f))) = find_goal state;
-    val (exp_tac, tacs) = ProofContext.export_wrt true inner (Some outer);
+    val exp_tac = ProofContext.export_wrt true inner (Some outer);
     fun exp_rule rule =
       let
         val _ = print_rule rule;
-        val thmq = FINDGOAL (Tactic.rtac rule THEN' RANGE tacs) thm;
+        val thmq = FINDGOAL (refine_tac rule) thm;
       in Seq.map (fn th => map_goal I (K ((result, (facts, th)), f)) state) thmq end;
   in raw_rule |> exp_tac |> (Seq.flat o Seq.map exp_rule) end;
 
 fun export_thm inner thm =
-  let val (exp_tac, tacs) = ProofContext.export_wrt false inner None in
-    (case Seq.chop (2, (exp_tac THEN RANGE tacs 1) thm) of
+  let val exp_tac = ProofContext.export_wrt false inner None in
+    (case Seq.chop (2, exp_tac thm) of
       ([thm'], _) => thm'
     | ([], _) => raise THM ("export: failed", 0, [thm])
     | _ => raise THM ("export: more than one result", 0, [thm]))
@@ -437,9 +441,9 @@
     None => Seq.single (reset_facts state)
   | Some thms =>
       let
-        val (exp_tac, tacs) =
+        val exp_tac =
           ProofContext.export_wrt false (context_of inner_state) (Some (context_of state));
-        val thmqs = map (exp_tac THEN RANGE tacs 1) thms;
+        val thmqs = map exp_tac thms;
       in Seq.map (fn ths => put_facts (Some ths) state) (Seq.commute thmqs) end);
 
 
@@ -460,7 +464,7 @@
     val tsig = Sign.tsig_of sign;
 
     val casms = flat (map #1 (assumptions state));
-    val bad_hyps = Library.gen_rems Term.aconv (hyps, map (Thm.term_of o Drule.mk_cgoal) casms);
+    val bad_hyps = Library.gen_rems Term.aconv (hyps, map Thm.term_of casms);
   in
     if not (null bad_hyps) then
       err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) bad_hyps))
@@ -518,9 +522,6 @@
 
 (* assume *)
 
-val hard_asm_tac = Tactic.etac Drule.triv_goal;
-val soft_asm_tac = Tactic.rtac Drule.triv_goal THEN' Tactic.norm_hhf_tac;
-
 local
 
 fun gen_assume f exp args state =
@@ -531,18 +532,19 @@
     these_factss (st, factss)
     |> put_thms ("prems", prems));
 
-fun simple_exporter tac1 tac2 =
-  (Seq.single oo Drule.implies_intr_list, fn is_goal => fn n =>
-    replicate n (Tactic.norm_hhf_tac THEN' (if is_goal then tac1 else tac2)));
+fun export_assume true = Seq.single oo Drule.implies_intr_goals
+  | export_assume false = Seq.single oo Drule.implies_intr_list;
+
+fun export_presume _ = export_assume false;
 
 in
 
 val assm = gen_assume ProofContext.assume;
 val assm_i = gen_assume ProofContext.assume_i;
-val assume = assm (simple_exporter hard_asm_tac soft_asm_tac);
-val assume_i = assm_i (simple_exporter hard_asm_tac soft_asm_tac);
-val presume = assm (simple_exporter soft_asm_tac soft_asm_tac);
-val presume_i = assm_i (simple_exporter soft_asm_tac soft_asm_tac);
+val assume = assm export_assume;
+val assume_i = assm_i export_assume;
+val presume = assm export_presume;
+val presume_i = assm_i export_presume;
 
 end;
 
@@ -676,7 +678,7 @@
     val outer_ctxt = context_of outer_state;
 
     val result = prep_result state t raw_thm;
-    val resultq = #1 (ProofContext.export_wrt false goal_ctxt (Some outer_ctxt)) result;
+    val resultq = ProofContext.export_wrt false goal_ctxt (Some outer_ctxt) result;
 
     val (atts, opt_solve) =
       (case kind of

--- a/src/Pure/Isar/proof_context.ML	Tue Oct 16 23:00:21 2001 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Oct 16 23:02:14 2001 +0200
@@ -42,7 +42,7 @@
   val generalizeT: context -> context -> typ -> typ
   val generalize: context -> context -> term -> term
   val find_free: term -> string -> term option
-  val export_wrt: bool -> context -> context option -> (thm -> thm Seq.seq) * (int -> tactic) list
+  val export_wrt: bool -> context -> context option -> thm -> thm Seq.seq
   val drop_schematic: indexname * term option -> indexname * term option
   val add_binds: (indexname * string option) list -> context -> context
   val add_binds_i: (indexname * term option) list -> context -> context
@@ -120,8 +120,7 @@
 
 (** datatype context **)
 
-type exporter =
-  (cterm list -> thm -> thm Seq.seq) * (bool -> int -> (int -> tactic) list);
+type exporter = bool -> cterm list -> thm -> thm Seq.seq;
 
 datatype context =
   Context of
@@ -578,40 +577,31 @@
 
 fun find_free t x = foldl_aterms (get_free x) (None, t);
 
-
-local
-
-fun export tfrees fixes goal_asms thm =
-  thm
-  |> Tactic.norm_hhf
-  |> Seq.EVERY (rev (map op |> goal_asms))
-  |> Seq.map (fn rule =>
-    let
-      val {sign, prop, maxidx, ...} = Thm.rep_thm rule;
-      val frees = map (Thm.cterm_of sign) (mapfilter (find_free prop) fixes);
-    in
-      rule
-      |> Drule.forall_intr_list frees
-      |> Tactic.norm_hhf
-      |> Drule.tvars_intr_list tfrees
-    end);
-
 fun diff_context inner None = (gen_tfrees inner None, fixed_names inner, assumptions inner)
   | diff_context inner (Some outer) =
       (gen_tfrees inner (Some outer),
         fixed_names inner \\ fixed_names outer,
         Library.drop (length (assumptions outer), assumptions inner));
 
-in
-
 fun export_wrt is_goal inner opt_outer =
   let
     val (tfrees, fixes, asms) = diff_context inner opt_outer;
-    val goal_asms = map (fn (cprops, (exp, _)) => (map Drule.mk_cgoal cprops, exp)) asms;
-    val tacs = flat (map (fn (cprops, (_, f)) => f is_goal (length cprops)) asms);
-  in (export tfrees fixes goal_asms, tacs) end;
-
-end;
+    val exp_asms = map (fn (cprops, exp) => exp is_goal cprops) asms;
+  in fn thm =>
+    thm
+    |> Tactic.norm_hhf
+    |> Seq.EVERY (rev exp_asms)
+    |> Seq.map (fn rule =>
+      let
+        val {sign, prop, ...} = Thm.rep_thm rule;
+        val frees = map (Thm.cterm_of sign) (mapfilter (find_free prop) fixes);
+      in
+        rule
+        |> Drule.forall_intr_list frees
+        |> Tactic.norm_hhf
+        |> Drule.tvars_intr_list tfrees
+      end)
+  end;
 
 
 
@@ -849,7 +839,7 @@
 fun add_assm (ctxt, ((name, attrs), props)) =
   let
     val cprops = map (Thm.cterm_of (sign_of ctxt)) props;
-    val asms = map (Tactic.norm_hhf o Drule.assume_goal) cprops;
+    val asms = map (Tactic.norm_hhf o Thm.assume) cprops;
 
     val ths = map (fn th => ([th], [])) asms;
     val (ctxt', [(_, thms)]) =