# HG changeset patch
# User wenzelm
# Date 1248982035 -7200
# Node ID 47278524df55c0e0e1044b3a256834a8f5a545ac
# Parent  c14aeb0bcce45fceca7f596a9ced4caa4ab51670# Parent  ab9b66c2bbca7f655fc0e40b374346658f939e1a
merged

diff -r c14aeb0bcce4 -r 47278524df55 src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Thu Jul 30 08:18:22 2009 +0200
+++ b/src/CCL/Wfd.thy	Thu Jul 30 21:27:15 2009 +0200
@@ -498,13 +498,14 @@
   structure Data = Named_Thms(val name = "eval" val description = "evaluation rules");
 in
 
-fun eval_tac ctxt ths i =
-  DEPTH_SOLVE_1 (resolve_tac (ths @ Data.get ctxt) i ORELSE assume_tac i);
+fun eval_tac ths =
+  Subgoal.FOCUS_PREMS (fn {context, prems, ...} =>
+    DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get context) 1));
 
 val eval_setup =
   Data.setup #>
   Method.setup @{binding eval}
-    (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ctxt ths)))
+    (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ths ctxt)))
     "evaluation";
 
 end;
diff -r c14aeb0bcce4 -r 47278524df55 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Thu Jul 30 08:18:22 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Jul 30 21:27:15 2009 +0200
@@ -3337,7 +3337,7 @@
       REPEAT (FIRST' [etac @{thm intervalE},
                       etac @{thm meta_eqE},
                       rtac @{thm impI}] i)
-      THEN FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) @{context} i
+      THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) @{context} i
       THEN TRY (filter_prems_tac (K false) i)
       THEN DETERM (Reflection.genreify_tac ctxt form_equations NONE i)
       THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
diff -r c14aeb0bcce4 -r 47278524df55 src/HOL/Prolog/prolog.ML
--- a/src/HOL/Prolog/prolog.ML	Thu Jul 30 08:18:22 2009 +0200
+++ b/src/HOL/Prolog/prolog.ML	Thu Jul 30 21:27:15 2009 +0200
@@ -67,7 +67,7 @@
         imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
         imp_all];         (* "((!x. D) :- G) = (!x. D :- G)" *)
 
-(*val hyp_resolve_tac = FOCUS (fn {prems, ...} =>
+(*val hyp_resolve_tac = Subgoal.FOCUS_PREMS (fn {prems, ...} =>
                                   resolve_tac (maps atomizeD prems) 1);
   -- is nice, but cannot instantiate unknowns in the assumptions *)
 fun hyp_resolve_tac i st = let
diff -r c14aeb0bcce4 -r 47278524df55 src/HOL/Tools/cnf_funcs.ML
--- a/src/HOL/Tools/cnf_funcs.ML	Thu Jul 30 08:18:22 2009 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML	Thu Jul 30 21:27:15 2009 +0200
@@ -517,7 +517,7 @@
 
 fun cnf_rewrite_tac ctxt i =
 	(* cut the CNF formulas as new premises *)
-	FOCUS (fn {prems, ...} =>
+	Subgoal.FOCUS (fn {prems, ...} =>
 		let
 		  val thy = ProofContext.theory_of ctxt
 			val cnf_thms = map (make_cnf_thm thy o HOLogic.dest_Trueprop o Thm.prop_of) prems
@@ -540,7 +540,7 @@
 
 fun cnfx_rewrite_tac ctxt i =
 	(* cut the CNF formulas as new premises *)
-	FOCUS (fn {prems, ...} =>
+	Subgoal.FOCUS (fn {prems, ...} =>
 		let
 		  val thy = ProofContext.theory_of ctxt;
 			val cnfx_thms = map (make_cnfx_thm thy o HOLogic.dest_Trueprop o prop_of) prems
diff -r c14aeb0bcce4 -r 47278524df55 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Thu Jul 30 08:18:22 2009 +0200
+++ b/src/HOL/Tools/meson.ML	Thu Jul 30 21:27:15 2009 +0200
@@ -586,9 +586,9 @@
   SELECT_GOAL
     (EVERY [ObjectLogic.atomize_prems_tac 1,
             rtac ccontr 1,
-            FOCUS (fn {context = ctxt', prems = negs, ...} =>
+            Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
                       EVERY1 [skolemize_prems_tac ctxt negs,
-                              FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
+                              Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
   handle THM _ => no_tac st;    (*probably from make_meta_clause, not first-order*)
 
 (** Best-first search versions **)
diff -r c14aeb0bcce4 -r 47278524df55 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Thu Jul 30 08:18:22 2009 +0200
+++ b/src/HOL/Tools/record.ML	Thu Jul 30 21:27:15 2009 +0200
@@ -2161,7 +2161,7 @@
       fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
         st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1
         THEN res_inst_tac context [((rN, 0), s')] cases_scheme 1
-        THEN (FOCUS (fn {prems, ...} => equality_tac prems) context 1))
+        THEN (Subgoal.FOCUS (fn {prems, ...} => equality_tac prems) context 1))
              (* simp_all_tac ss (sel_convs) would also work but is less efficient *)
       end);
      val equality = timeit_msg "record equality proof:" equality_prf;
diff -r c14aeb0bcce4 -r 47278524df55 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Thu Jul 30 08:18:22 2009 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Thu Jul 30 21:27:15 2009 +0200
@@ -517,7 +517,7 @@
   SUBGOAL (fn (prop, i) =>
     let val ts = Logic.strip_assums_hyp prop in
       EVERY'
-       [FOCUS
+       [Subgoal.FOCUS
          (fn {prems, ...} =>
            (Method.insert_tac
              (map forall_intr_vars (neg_clausify prems)) i)) ctxt,
diff -r c14aeb0bcce4 -r 47278524df55 src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Thu Jul 30 08:18:22 2009 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Thu Jul 30 21:27:15 2009 +0200
@@ -411,7 +411,7 @@
 (* ------------------------------------------------------------------------- *)
 
 fun rawsat_tac ctxt i =
-  FOCUS (fn {prems, ...} => rtac (rawsat_thm (map cprop_of prems)) 1) ctxt i;
+  Subgoal.FOCUS (fn {prems, ...} => rtac (rawsat_thm (map cprop_of prems)) 1) ctxt i;
 
 (* ------------------------------------------------------------------------- *)
 (* pre_cnf_tac: converts the i-th subgoal                                    *)
diff -r c14aeb0bcce4 -r 47278524df55 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Thu Jul 30 08:18:22 2009 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Jul 30 21:27:15 2009 +0200
@@ -788,7 +788,7 @@
           all_tac) THEN
           PRIMITIVE (trace_thm ctxt "State after neqE:") THEN
           (* use theorems generated from the actual justifications *)
-          FOCUS (fn {prems, ...} => rtac (mkthm ss prems j) 1) ctxt i
+          Subgoal.FOCUS (fn {prems, ...} => rtac (mkthm ss prems j) 1) ctxt i
     in
       (* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *)
       DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN
diff -r c14aeb0bcce4 -r 47278524df55 src/Provers/order.ML
--- a/src/Provers/order.ML	Thu Jul 30 08:18:22 2009 +0200
+++ b/src/Provers/order.ML	Thu Jul 30 21:27:15 2009 +0200
@@ -1235,12 +1235,12 @@
    val prfs = gen_solve mkconcl thy (lesss, C);
    val (subgoals, prf) = mkconcl decomp less_thms thy C;
   in
-   FOCUS (fn {prems = asms, ...} =>
+   Subgoal.FOCUS (fn {prems = asms, ...} =>
      let val thms = map (prove (prems @ asms)) prfs
      in rtac (prove thms prf) 1 end) ctxt n st
   end
   handle Contr p =>
-      (FOCUS (fn {prems = asms, ...} => rtac (prove asms p) 1) ctxt n st
+      (Subgoal.FOCUS (fn {prems = asms, ...} => rtac (prove asms p) 1) ctxt n st
         handle Subscript => Seq.empty)
    | Cannot => Seq.empty
    | Subscript => Seq.empty)
diff -r c14aeb0bcce4 -r 47278524df55 src/Provers/quasi.ML
--- a/src/Provers/quasi.ML	Thu Jul 30 08:18:22 2009 +0200
+++ b/src/Provers/quasi.ML	Thu Jul 30 21:27:15 2009 +0200
@@ -551,7 +551,7 @@
 
 fun trans_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
  let
-  val thy = Thm.theory_of_thm st;
+  val thy = ProofContext.theory_of ctxt;
   val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
   val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
   val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
@@ -560,11 +560,11 @@
 
   val (subgoal, prf) = mkconcl_trans thy C;
  in
-  FOCUS (fn {prems, ...} =>
+  Subgoal.FOCUS (fn {prems, ...} =>
     let val thms = map (prove prems) prfs
     in rtac (prove thms prf) 1 end) ctxt n st
  end
- handle Contr p => FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
+ handle Contr p => Subgoal.FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
   | Cannot  => Seq.empty);
 
 
@@ -572,7 +572,7 @@
 
 fun quasi_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
  let
-  val thy = Thm.theory_of_thm st;
+  val thy = ProofContext.theory_of ctxt
   val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
   val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
   val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
@@ -580,12 +580,12 @@
   val prfs = solveQuasiOrder thy (lesss, C);
   val (subgoals, prf) = mkconcl_quasi thy C;
  in
-  FOCUS (fn {prems, ...} =>
+  Subgoal.FOCUS (fn {prems, ...} =>
     let val thms = map (prove prems) prfs
     in rtac (prove thms prf) 1 end) ctxt n st
  end
  handle Contr p =>
-    (FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
+    (Subgoal.FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
       handle Subscript => Seq.empty)
   | Cannot => Seq.empty
   | Subscript => Seq.empty);
diff -r c14aeb0bcce4 -r 47278524df55 src/Provers/trancl.ML
--- a/src/Provers/trancl.ML	Thu Jul 30 08:18:22 2009 +0200
+++ b/src/Provers/trancl.ML	Thu Jul 30 21:27:15 2009 +0200
@@ -533,7 +533,7 @@
 
 fun trancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
  let
-  val thy = Thm.theory_of_thm st;
+  val thy = ProofContext.theory_of ctxt;
   val Hs = Logic.strip_assums_hyp A;
   val C = Logic.strip_assums_concl A;
   val (rel, subgoals, prf) = mkconcl_trancl C;
@@ -541,7 +541,7 @@
   val prems = flat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)));
   val prfs = solveTrancl (prems, C);
  in
-  FOCUS (fn {prems, ...} =>
+  Subgoal.FOCUS (fn {prems, ...} =>
     let val thms = map (prove thy rel prems) prfs
     in rtac (prove thy rel thms prf) 1 end) ctxt n st
  end
@@ -550,7 +550,7 @@
 
 fun rtrancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
  let
-  val thy = Thm.theory_of_thm st;
+  val thy = ProofContext.theory_of ctxt;
   val Hs = Logic.strip_assums_hyp A;
   val C = Logic.strip_assums_concl A;
   val (rel, subgoals, prf) = mkconcl_rtrancl C;
@@ -558,7 +558,7 @@
   val prems = flat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)));
   val prfs = solveRtrancl (prems, C);
  in
-  FOCUS (fn {prems, ...} =>
+  Subgoal.FOCUS (fn {prems, ...} =>
     let val thms = map (prove thy rel prems) prfs
     in rtac (prove thy rel thms prf) 1 end) ctxt n st
  end
diff -r c14aeb0bcce4 -r 47278524df55 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu Jul 30 08:18:22 2009 +0200
+++ b/src/Pure/more_thm.ML	Thu Jul 30 21:27:15 2009 +0200
@@ -41,6 +41,11 @@
   val elim_implies: thm -> thm -> thm
   val forall_elim_var: int -> thm -> thm
   val forall_elim_vars: int -> thm -> thm
+  val certify_inst: theory ->
+    ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
+    (ctyp * ctyp) list * (cterm * cterm) list
+  val certify_instantiate:
+    ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
   val unvarify: thm -> thm
   val close_derivation: thm -> thm
   val add_axiom: binding * term -> theory -> thm * theory
@@ -269,24 +274,29 @@
 end;
 
 
+(* certify_instantiate *)
+
+fun certify_inst thy (instT, inst) =
+  (map (fn (v, T) => (Thm.ctyp_of thy (TVar v), Thm.ctyp_of thy T)) instT,
+    map (fn (v, t) => (Thm.cterm_of thy (Var v), Thm.cterm_of thy t)) inst);
+
+fun certify_instantiate insts th =
+  Thm.instantiate (certify_inst (Thm.theory_of_thm th) insts) th;
+
+
 (* unvarify: global schematic variables *)
 
 fun unvarify th =
   let
-    val thy = Thm.theory_of_thm th;
-    val cert = Thm.cterm_of thy;
-    val certT = Thm.ctyp_of thy;
-
     val prop = Thm.full_prop_of th;
     val _ = map Logic.unvarify (prop :: Thm.hyps_of th)
       handle TERM (msg, _) => raise THM (msg, 0, [th]);
 
-    val instT0 = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S)));
-    val instT = map (fn (v, T) => (certT (TVar v), certT T)) instT0;
+    val instT = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S)));
     val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) =>
-      let val T' = Term_Subst.instantiateT instT0 T
-      in (cert (Var ((a, i), T')), cert (Free ((a, T')))) end);
-  in Thm.instantiate (instT, inst) th end;
+      let val T' = Term_Subst.instantiateT instT T
+      in (((a, i), T'), Free ((a, T'))) end);
+  in certify_instantiate (instT, inst) th end;
 
 
 (* close_derivation *)
diff -r c14aeb0bcce4 -r 47278524df55 src/Pure/subgoal.ML
--- a/src/Pure/subgoal.ML	Thu Jul 30 08:18:22 2009 +0200
+++ b/src/Pure/subgoal.ML	Thu Jul 30 21:27:15 2009 +0200
@@ -1,20 +1,23 @@
 (*  Title:      Pure/subgoal.ML
     Author:     Makarius
 
-Tactical operations with explicit subgoal focus, based on
-canonical proof decomposition (similar to fix/assume/show).
+Tactical operations with explicit subgoal focus, based on canonical
+proof decomposition.  The "visible" part of the text within the
+context is fixed, the remaining goal may be schematic.
 *)
 
 signature SUBGOAL =
 sig
   type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
-    asms: cterm list, concl: cterm, schematics: ctyp list * cterm list}
+    asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list}
+  val focus_params: Proof.context -> int -> thm -> focus * thm
+  val focus_prems: Proof.context -> int -> thm -> focus * thm
   val focus: Proof.context -> int -> thm -> focus * thm
-  val focus_params: Proof.context -> int -> thm -> focus * thm
   val retrofit: Proof.context -> Proof.context -> (string * cterm) list -> cterm list ->
     int -> thm -> thm -> thm Seq.seq
+  val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic
+  val FOCUS_PREMS: (focus -> tactic) -> Proof.context -> int -> tactic
   val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic
-  val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic
   val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic
 end;
 
@@ -24,24 +27,35 @@
 (* focus *)
 
 type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
-  asms: cterm list, concl: cterm, schematics: ctyp list * cterm list};
+  asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list};
 
-fun gen_focus params_only ctxt i st =
+fun gen_focus (do_prems, do_concl) ctxt i raw_st =
   let
-    val ((schematics, [st']), ctxt') =
-      Variable.import true [Simplifier.norm_hhf_protect st] ctxt;
-    val ((params, goal), ctxt'') = Variable.focus_subgoal i st' ctxt';
+    val st = Simplifier.norm_hhf_protect raw_st;
+    val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
+    val ((params, goal), ctxt2) = Variable.focus (Thm.cprem_of st' i) ctxt1;
+
     val (asms, concl) =
-      if params_only then ([], goal)
-      else (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal);
-    val (prems, context) = Assumption.add_assumes asms ctxt'';
+      if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
+      else ([], goal);
+    val text = asms @ (if do_concl then [concl] else []);
+
+    val ((_, schematic_terms), ctxt3) =
+      Variable.import_inst true (map Thm.term_of text) ctxt2
+      |>> Thm.certify_inst (Thm.theory_of_thm raw_st);
+
+    val schematics = (schematic_types, schematic_terms);
+    val asms' = map (Thm.instantiate_cterm schematics) asms;
+    val concl' = Thm.instantiate_cterm schematics concl;
+    val (prems, context) = Assumption.add_assumes asms' ctxt3;
   in
     ({context = context, params = params, prems = prems,
-      asms = asms, concl = concl, schematics = schematics}, Goal.init concl)
+      asms = asms', concl = concl', schematics = schematics}, Goal.init concl')
   end;
 
-val focus = gen_focus false;
-val focus_params = gen_focus true;
+val focus_params = gen_focus (false, false);
+val focus_prems = gen_focus (true, false);
+val focus = gen_focus (true, true);
 
 
 (* lift and retrofit *)
@@ -51,29 +65,40 @@
   ----------------
   B ['b, y params]
 *)
-fun lift_import params th ctxt =
+fun lift_import idx params th ctxt =
   let
-    val cert = Thm.cterm_of (Thm.theory_of_thm th);
+    val cert = Thm.cterm_of (ProofContext.theory_of ctxt);
     val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
 
     val Ts = map (#T o Thm.rep_cterm) params;
     val ts = map Thm.term_of params;
 
-    val vars = rev (Term.add_vars (Thm.full_prop_of th') []);
+    val prop = Thm.full_prop_of th';
+    val concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [];
+    val vars = rev (Term.add_vars prop []);
     val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
-    fun var_inst (v as (_, T)) y =
-      (cert (Var v), cert (list_comb (Free (y, Ts ---> T), ts)));
-    val th'' = Thm.instantiate ([], map2 var_inst vars ys) th';
-  in (th'', ctxt'') end;
+
+    fun var_inst v y =
+      let
+        val ((x, i), T) = v;
+        val (U, args) =
+          if member (op =) concl_vars v then (T, [])
+          else (Ts ---> T, ts);
+        val u = Free (y, U);
+        in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
+    val (inst1, inst2) = split_list (map (pairself (pairself cert)) (map2 var_inst vars ys));
+
+    val th'' = Thm.instantiate ([], inst1) th';
+  in ((inst2, th''), ctxt'') end;
 
 (*
-      [x, A x]
+       [x, A x]
           :
-      B x ==> C
+       B x ==> C
   ------------------
   [!!x. A x ==> B x]
-         :
-         C
+          :
+          C
 *)
 fun lift_subgoals params asms th =
   let
@@ -87,36 +112,37 @@
 
 fun retrofit ctxt1 ctxt0 params asms i st1 st0 =
   let
+    val idx = Thm.maxidx_of st0 + 1;
     val ps = map #2 params;
-    val (st2, ctxt2) = lift_import ps st1 ctxt1;
+    val ((subgoal_inst, st2), ctxt2) = lift_import idx ps st1 ctxt1;
     val (subgoals, st3) = lift_subgoals params asms st2;
     val result = st3
       |> Goal.conclude
       |> Drule.implies_intr_list asms
       |> Drule.forall_intr_list ps
       |> Drule.implies_intr_list subgoals
-      |> singleton (Variable.export ctxt2 ctxt0)
-      |> Drule.zero_var_indexes
-      |> Drule.incr_indexes st0;
+      |> fold_rev (Thm.forall_intr o #1) subgoal_inst
+      |> fold (Thm.forall_elim o #2) subgoal_inst
+      |> Thm.adjust_maxidx_thm idx
+      |> singleton (Variable.export ctxt2 ctxt0);
   in Thm.compose_no_flatten false (result, Thm.nprems_of st1) i st0 end;
 
 
 (* tacticals *)
 
-fun GEN_FOCUS params_only tac ctxt i st =
+fun GEN_FOCUS flags tac ctxt i st =
   if Thm.nprems_of st < i then Seq.empty
   else
-    let val (args as {context, params, asms, ...}, st') = gen_focus params_only ctxt i st;
+    let val (args as {context, params, asms, ...}, st') = gen_focus flags ctxt i st;
     in Seq.lifts (retrofit context ctxt params asms i) (tac args st') st end;
 
-val FOCUS = GEN_FOCUS false;
-val FOCUS_PARAMS = GEN_FOCUS true;
+val FOCUS_PARAMS = GEN_FOCUS (false, false);
+val FOCUS_PREMS = GEN_FOCUS (true, false);
+val FOCUS = GEN_FOCUS (true, true);
 
 fun SUBPROOF tac = FOCUS (FILTER Thm.no_prems o tac);
 
 end;
 
-val FOCUS = Subgoal.FOCUS;
-val FOCUS_PARAMS = Subgoal.FOCUS_PARAMS;
 val SUBPROOF = Subgoal.SUBPROOF;
 
diff -r c14aeb0bcce4 -r 47278524df55 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Thu Jul 30 08:18:22 2009 +0200
+++ b/src/Pure/variable.ML	Thu Jul 30 21:27:15 2009 +0200
@@ -51,10 +51,10 @@
     (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context
   val importT_terms: term list -> Proof.context -> term list * Proof.context
   val import_terms: bool -> term list -> Proof.context -> term list * Proof.context
-  val importT: thm list -> Proof.context -> (ctyp list * thm list) * Proof.context
+  val importT: thm list -> Proof.context -> ((ctyp * ctyp) list * thm list) * Proof.context
   val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
   val import: bool -> thm list -> Proof.context ->
-    ((ctyp list * cterm list) * thm list) * Proof.context
+    (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context
   val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
   val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
   val focus: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
@@ -427,11 +427,10 @@
 fun importT ths ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
-    val certT = Thm.ctyp_of thy;
     val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
-    val instT' = map (fn (v, T) => (certT (TVar v), certT T)) instT;
-    val ths' = map (Thm.instantiate (instT', [])) ths;
-  in ((map #2 instT', ths'), ctxt') end;
+    val insts' as (instT', _) = Thm.certify_inst thy (instT, []);
+    val ths' = map (Thm.instantiate insts') ths;
+  in ((instT', ths'), ctxt') end;
 
 fun import_prf is_open prf ctxt =
   let
@@ -442,13 +441,10 @@
 fun import is_open ths ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
-    val cert = Thm.cterm_of thy;
-    val certT = Thm.ctyp_of thy;
-    val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
-    val instT' = map (fn (v, T) => (certT (TVar v), certT T)) instT;
-    val inst' = map (fn (v, t) => (cert (Var v), cert t)) inst;
-    val ths' = map (Thm.instantiate (instT', inst')) ths;
-  in (((map #2 instT', map #2 inst'), ths'), ctxt') end;
+    val (insts, ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
+    val insts' = Thm.certify_inst thy insts;
+    val ths' = map (Thm.instantiate insts') ths;
+  in ((insts', ths'), ctxt') end;
 
 
 (* import/export *)