Variable.focus: named parameters;

--- a/src/Pure/Isar/element.ML	Sun Jul 26 13:12:53 2009 +0200
+++ b/src/Pure/Isar/element.ML	Sun Jul 26 13:12:54 2009 +0200
@@ -213,7 +213,7 @@
   let
     val ((xs, prop'), ctxt') = Variable.focus prop ctxt;
     val As = Logic.strip_imp_prems (Thm.term_of prop');
-  in ((Binding.empty, (map (fix o Term.dest_Free o Thm.term_of) xs, As)), ctxt') end;
+  in ((Binding.empty, (map (fix o Term.dest_Free o Thm.term_of o #2) xs, As)), ctxt') end;
 
 in
 

--- a/src/Pure/Isar/obtain.ML	Sun Jul 26 13:12:53 2009 +0200
+++ b/src/Pure/Isar/obtain.ML	Sun Jul 26 13:12:54 2009 +0200
@@ -44,7 +44,7 @@
   val obtain_i: string -> (binding * typ option * mixfix) list ->
     (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
   val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
-    (cterm list * thm list) * Proof.context
+    ((string * cterm) list * thm list) * Proof.context
   val guess: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
   val guess_i: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
 end;
@@ -200,7 +200,7 @@
     val obtain_rule = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule';
     val ((params, stmt), fix_ctxt) = Variable.focus (Thm.cprem_of obtain_rule 1) ctxt';
     val (prems, ctxt'') =
-      Assumption.add_assms (obtain_export fix_ctxt obtain_rule params)
+      Assumption.add_assms (obtain_export fix_ctxt obtain_rule (map #2 params))
         (Drule.strip_imp_prems stmt) fix_ctxt;
   in ((params, prems), ctxt'') end;
 

--- a/src/Pure/variable.ML	Sun Jul 26 13:12:53 2009 +0200
+++ b/src/Pure/variable.ML	Sun Jul 26 13:12:54 2009 +0200
@@ -57,8 +57,8 @@
     ((ctyp list * 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 -> (cterm list * cterm) * Proof.context
-  val focus_subgoal: int -> thm -> Proof.context -> (cterm list * cterm) * Proof.context
+  val focus: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
+  val focus_subgoal: int -> thm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
   val warn_extra_tfrees: Proof.context -> Proof.context -> unit
   val polymorphic_types: Proof.context -> term list -> (indexname * sort) list * term list
   val polymorphic: Proof.context -> term list -> term list
@@ -477,7 +477,7 @@
     val ps' = ListPair.map (cert o Free) (xs', Ts);
     val goal' = fold forall_elim_prop ps' goal;
     val ctxt'' = ctxt' |> fold (declare_constraints o Thm.term_of) ps';
-  in ((ps', goal'), ctxt'') end;
+  in ((xs ~~ ps', goal'), ctxt'') end;
 
 fun focus_subgoal i st =
   let

--- a/src/Tools/coherent.ML	Sun Jul 26 13:12:53 2009 +0200
+++ b/src/Tools/coherent.ML	Sun Jul 26 13:12:54 2009 +0200
@@ -215,7 +215,7 @@
 fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context, ...} =>
   rtac (rulify_elim_conv concl RS equal_elim_rule2) 1 THEN
   SUBPROOF (fn {prems = prems', concl, context, ...} =>
-    let val xs = map term_of params @
+    let val xs = map (term_of o #2) params @
       map (fn (_, s) => Free (s, the (Variable.default_type context s)))
         (Variable.fixes_of context)
     in