Variable.focus: named parameters;
authorwenzelm
Sun Jul 26 13:12:54 2009 +0200 (2009-07-26)
changeset 3219982c4c570310a
parent 32198 9bdd47909ea8
child 32200 2bd8ab91a426
Variable.focus: named parameters;
src/Pure/Isar/element.ML
src/Pure/Isar/obtain.ML
src/Pure/variable.ML
src/Tools/coherent.ML
     1.1 --- a/src/Pure/Isar/element.ML	Sun Jul 26 13:12:53 2009 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Sun Jul 26 13:12:54 2009 +0200
     1.3 @@ -213,7 +213,7 @@
     1.4    let
     1.5      val ((xs, prop'), ctxt') = Variable.focus prop ctxt;
     1.6      val As = Logic.strip_imp_prems (Thm.term_of prop');
     1.7 -  in ((Binding.empty, (map (fix o Term.dest_Free o Thm.term_of) xs, As)), ctxt') end;
     1.8 +  in ((Binding.empty, (map (fix o Term.dest_Free o Thm.term_of o #2) xs, As)), ctxt') end;
     1.9  
    1.10  in
    1.11  
     2.1 --- a/src/Pure/Isar/obtain.ML	Sun Jul 26 13:12:53 2009 +0200
     2.2 +++ b/src/Pure/Isar/obtain.ML	Sun Jul 26 13:12:54 2009 +0200
     2.3 @@ -44,7 +44,7 @@
     2.4    val obtain_i: string -> (binding * typ option * mixfix) list ->
     2.5      (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
     2.6    val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
     2.7 -    (cterm list * thm list) * Proof.context
     2.8 +    ((string * cterm) list * thm list) * Proof.context
     2.9    val guess: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
    2.10    val guess_i: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
    2.11  end;
    2.12 @@ -200,7 +200,7 @@
    2.13      val obtain_rule = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule';
    2.14      val ((params, stmt), fix_ctxt) = Variable.focus (Thm.cprem_of obtain_rule 1) ctxt';
    2.15      val (prems, ctxt'') =
    2.16 -      Assumption.add_assms (obtain_export fix_ctxt obtain_rule params)
    2.17 +      Assumption.add_assms (obtain_export fix_ctxt obtain_rule (map #2 params))
    2.18          (Drule.strip_imp_prems stmt) fix_ctxt;
    2.19    in ((params, prems), ctxt'') end;
    2.20  
     3.1 --- a/src/Pure/variable.ML	Sun Jul 26 13:12:53 2009 +0200
     3.2 +++ b/src/Pure/variable.ML	Sun Jul 26 13:12:54 2009 +0200
     3.3 @@ -57,8 +57,8 @@
     3.4      ((ctyp list * cterm list) * thm list) * Proof.context
     3.5    val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
     3.6    val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
     3.7 -  val focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context
     3.8 -  val focus_subgoal: int -> thm -> Proof.context -> (cterm list * cterm) * Proof.context
     3.9 +  val focus: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
    3.10 +  val focus_subgoal: int -> thm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
    3.11    val warn_extra_tfrees: Proof.context -> Proof.context -> unit
    3.12    val polymorphic_types: Proof.context -> term list -> (indexname * sort) list * term list
    3.13    val polymorphic: Proof.context -> term list -> term list
    3.14 @@ -477,7 +477,7 @@
    3.15      val ps' = ListPair.map (cert o Free) (xs', Ts);
    3.16      val goal' = fold forall_elim_prop ps' goal;
    3.17      val ctxt'' = ctxt' |> fold (declare_constraints o Thm.term_of) ps';
    3.18 -  in ((ps', goal'), ctxt'') end;
    3.19 +  in ((xs ~~ ps', goal'), ctxt'') end;
    3.20  
    3.21  fun focus_subgoal i st =
    3.22    let
     4.1 --- a/src/Tools/coherent.ML	Sun Jul 26 13:12:53 2009 +0200
     4.2 +++ b/src/Tools/coherent.ML	Sun Jul 26 13:12:54 2009 +0200
     4.3 @@ -215,7 +215,7 @@
     4.4  fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context, ...} =>
     4.5    rtac (rulify_elim_conv concl RS equal_elim_rule2) 1 THEN
     4.6    SUBPROOF (fn {prems = prems', concl, context, ...} =>
     4.7 -    let val xs = map term_of params @
     4.8 +    let val xs = map (term_of o #2) params @
     4.9        map (fn (_, s) => Free (s, the (Variable.default_type context s)))
    4.10          (Variable.fixes_of context)
    4.11      in