# HG changeset patch # User wenzelm # Date 1272306650 -7200 # Node ID bbd742107f56e091d5d3623e9bf3495423272e71 # Parent 7b92238454d695345b63ee24b9cfe81ee1f0e464 eliminanated some unreferenced identifiers; tuned; diff -r 7b92238454d6 -r bbd742107f56 src/Pure/Isar/overloading.ML --- a/src/Pure/Isar/overloading.ML Mon Apr 26 16:08:04 2010 +0200 +++ b/src/Pure/Isar/overloading.ML Mon Apr 26 20:30:50 2010 +0200 @@ -67,8 +67,8 @@ fun improve_term_check ts ctxt = let - val { primary_constraints, secondary_constraints, improve, subst, - consider_abbrevs, passed, ... } = ImprovableSyntax.get ctxt; + val { secondary_constraints, improve, subst, consider_abbrevs, passed, ... } = + ImprovableSyntax.get ctxt; val tsig = (Sign.tsig_of o ProofContext.theory_of) ctxt; val is_abbrev = consider_abbrevs andalso ProofContext.abbrev_mode ctxt; val passed_or_abbrev = passed orelse is_abbrev; diff -r 7b92238454d6 -r bbd742107f56 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Mon Apr 26 16:08:04 2010 +0200 +++ b/src/Pure/Isar/proof.ML Mon Apr 26 20:30:50 2010 +0200 @@ -792,7 +792,7 @@ fun implicit_vars props = let - val (var_props, props') = take_prefix is_var props; + val (var_props, _) = take_prefix is_var props; val explicit_vars = fold Term.add_vars var_props []; val vars = filter_out (member (op =) explicit_vars) (fold Term.add_vars props []); in map (Logic.mk_term o Var) vars end; @@ -845,11 +845,10 @@ fun generic_qed after_ctxt state = let - val (goal_ctxt, {statement, goal, after_qed, ...}) = current_goal state; + val (goal_ctxt, {statement = (_, stmt, _), goal, after_qed, ...}) = current_goal state; val outer_state = state |> close_block; val outer_ctxt = context_of outer_state; - val ((_, pos), stmt, _) = statement; val props = flat (tl stmt) |> Variable.exportT_terms goal_ctxt outer_ctxt; diff -r 7b92238454d6 -r bbd742107f56 src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Mon Apr 26 16:08:04 2010 +0200 +++ b/src/Pure/Isar/rule_cases.ML Mon Apr 26 20:30:50 2010 +0200 @@ -368,7 +368,7 @@ map (Name.internal o Name.clean o fst) (Logic.strip_params prem) in Logic.list_rename_params (xs, prem) end; fun rename_prems prop = - let val (As, C) = Logic.strip_horn (Thm.prop_of rule) + let val (As, C) = Logic.strip_horn prop in Logic.list_implies (map rename As, C) end; in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end; diff -r 7b92238454d6 -r bbd742107f56 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Mon Apr 26 16:08:04 2010 +0200 +++ b/src/Pure/meta_simplifier.ML Mon Apr 26 20:30:50 2010 +0200 @@ -834,7 +834,6 @@ in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end handle THM _ => let - val thy = Thm.theory_of_thm thm; val _ $ _ $ prop0 = Thm.prop_of thm; in trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm'; diff -r 7b92238454d6 -r bbd742107f56 src/Pure/tactic.ML --- a/src/Pure/tactic.ML Mon Apr 26 16:08:04 2010 +0200 +++ b/src/Pure/tactic.ML Mon Apr 26 20:30:50 2010 +0200 @@ -188,9 +188,6 @@ let val (_, _, Bi, _) = dest_state (st, i) in Term.rename_wrt_term Bi (Logic.strip_params Bi) end; -(*params of subgoal i as they are printed*) -fun params_of_state i st = rev (innermost_params i st); - (*** Applications of cut_rl ***)