eliminanated some unreferenced identifiers;
authorwenzelm
Mon Apr 26 20:30:50 2010 +0200 (2010-04-26)
changeset 36354bbd742107f56
parent 36353 7b92238454d6
child 36355 aaa9933039b3
eliminanated some unreferenced identifiers;
tuned;
src/Pure/Isar/overloading.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/rule_cases.ML
src/Pure/meta_simplifier.ML
src/Pure/tactic.ML
     1.1 --- a/src/Pure/Isar/overloading.ML	Mon Apr 26 16:08:04 2010 +0200
     1.2 +++ b/src/Pure/Isar/overloading.ML	Mon Apr 26 20:30:50 2010 +0200
     1.3 @@ -67,8 +67,8 @@
     1.4  
     1.5  fun improve_term_check ts ctxt =
     1.6    let
     1.7 -    val { primary_constraints, secondary_constraints, improve, subst,
     1.8 -      consider_abbrevs, passed, ... } = ImprovableSyntax.get ctxt;
     1.9 +    val { secondary_constraints, improve, subst, consider_abbrevs, passed, ... } =
    1.10 +      ImprovableSyntax.get ctxt;
    1.11      val tsig = (Sign.tsig_of o ProofContext.theory_of) ctxt;
    1.12      val is_abbrev = consider_abbrevs andalso ProofContext.abbrev_mode ctxt;
    1.13      val passed_or_abbrev = passed orelse is_abbrev;
     2.1 --- a/src/Pure/Isar/proof.ML	Mon Apr 26 16:08:04 2010 +0200
     2.2 +++ b/src/Pure/Isar/proof.ML	Mon Apr 26 20:30:50 2010 +0200
     2.3 @@ -792,7 +792,7 @@
     2.4  
     2.5  fun implicit_vars props =
     2.6    let
     2.7 -    val (var_props, props') = take_prefix is_var props;
     2.8 +    val (var_props, _) = take_prefix is_var props;
     2.9      val explicit_vars = fold Term.add_vars var_props [];
    2.10      val vars = filter_out (member (op =) explicit_vars) (fold Term.add_vars props []);
    2.11    in map (Logic.mk_term o Var) vars end;
    2.12 @@ -845,11 +845,10 @@
    2.13  
    2.14  fun generic_qed after_ctxt state =
    2.15    let
    2.16 -    val (goal_ctxt, {statement, goal, after_qed, ...}) = current_goal state;
    2.17 +    val (goal_ctxt, {statement = (_, stmt, _), goal, after_qed, ...}) = current_goal state;
    2.18      val outer_state = state |> close_block;
    2.19      val outer_ctxt = context_of outer_state;
    2.20  
    2.21 -    val ((_, pos), stmt, _) = statement;
    2.22      val props =
    2.23        flat (tl stmt)
    2.24        |> Variable.exportT_terms goal_ctxt outer_ctxt;
     3.1 --- a/src/Pure/Isar/rule_cases.ML	Mon Apr 26 16:08:04 2010 +0200
     3.2 +++ b/src/Pure/Isar/rule_cases.ML	Mon Apr 26 20:30:50 2010 +0200
     3.3 @@ -368,7 +368,7 @@
     3.4          map (Name.internal o Name.clean o fst) (Logic.strip_params prem)
     3.5        in Logic.list_rename_params (xs, prem) end;
     3.6      fun rename_prems prop =
     3.7 -      let val (As, C) = Logic.strip_horn (Thm.prop_of rule)
     3.8 +      let val (As, C) = Logic.strip_horn prop
     3.9        in Logic.list_implies (map rename As, C) end;
    3.10    in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end;
    3.11  
     4.1 --- a/src/Pure/meta_simplifier.ML	Mon Apr 26 16:08:04 2010 +0200
     4.2 +++ b/src/Pure/meta_simplifier.ML	Mon Apr 26 20:30:50 2010 +0200
     4.3 @@ -834,7 +834,6 @@
     4.4    in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end
     4.5    handle THM _ =>
     4.6      let
     4.7 -      val thy = Thm.theory_of_thm thm;
     4.8        val _ $ _ $ prop0 = Thm.prop_of thm;
     4.9      in
    4.10        trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm';
     5.1 --- a/src/Pure/tactic.ML	Mon Apr 26 16:08:04 2010 +0200
     5.2 +++ b/src/Pure/tactic.ML	Mon Apr 26 20:30:50 2010 +0200
     5.3 @@ -188,9 +188,6 @@
     5.4    let val (_, _, Bi, _) = dest_state (st, i)
     5.5    in Term.rename_wrt_term Bi (Logic.strip_params Bi) end;
     5.6  
     5.7 -(*params of subgoal i as they are printed*)
     5.8 -fun params_of_state i st = rev (innermost_params i st);
     5.9 -
    5.10  
    5.11  (*** Applications of cut_rl ***)
    5.12