eliminated redundant bindings;

--- a/src/Pure/Concurrent/task_queue.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -125,7 +125,7 @@
 fun status (Queue {jobs, ...}) =
   let
     val (x, y, z) =
-      Task_Graph.fold (fn (task, ((_, job), (deps, _))) => fn (x, y, z) =>
+      Task_Graph.fold (fn (_, ((_, job), (deps, _))) => fn (x, y, z) =>
           (case job of
             Job _ => if null deps then (x + 1, y, z) else (x, y + 1, z)
           | Running _ => (x, y, z + 1)))

--- a/src/Pure/General/heap.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/General/heap.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -78,8 +78,8 @@
 
 nonfix upto;
 
-fun upto _ (h as Empty) = ([], h)
-  | upto limit (h as Heap (_, x, a, b)) =
+fun upto _ Empty = ([], Empty)
+  | upto limit (h as Heap (_, x, _, _)) =
       (case ord (x, limit) of
         GREATER => ([], h)
       | _ => upto limit (delete_min h) |>> cons x);

--- a/src/Pure/General/pretty.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/General/pretty.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -197,11 +197,11 @@
 fun setdepth dp = (depth := dp);
 
 local
-  fun pruning dp (Block (m, bes, indent, wd)) =
+  fun pruning dp (Block (m, bes, indent, _)) =
         if dp > 0
         then block_markup m (indent, map (pruning (dp - 1)) bes)
         else str "..."
-    | pruning dp e = e
+    | pruning _ e = e;
 in
   fun prune e = if ! depth > 0 then pruning (! depth) e else e;
 end;
@@ -219,7 +219,7 @@
   pos = 0,
   nl = 0};
 
-fun newline {tx, ind, pos, nl} : text =
+fun newline {tx, ind = _, pos = _, nl} : text =
  {tx = Buffer.add (Output.output "\n") tx,
   ind = Buffer.empty,
   pos = 0,
@@ -250,22 +250,22 @@
 (*Add the lengths of the expressions until the next Break; if no Break then
   include "after", to account for text following this block.*)
 fun breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after)
-  | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
-  | breakdist (Break _ :: es, after) = 0
+  | breakdist (String (_, len) :: es, after) = len + breakdist (es, after)
+  | breakdist (Break _ :: _, _) = 0
   | breakdist ([], after) = after;
 
 (*Search for the next break (at this or higher levels) and force it to occur.*)
 fun forcenext [] = []
-  | forcenext (Break (_, wd) :: es) = Break (true, 0) :: es
+  | forcenext (Break _ :: es) = Break (true, 0) :: es
   | forcenext (e :: es) = e :: forcenext es;
 
 (*es is list of expressions to print;
   blockin is the indentation of the current block;
   after is the width of the following context until next break.*)
 fun format ([], _, _) text = text
-  | format (e :: es, block as (blockind, blockin), after) (text as {ind, pos, nl, ...}) =
+  | format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) =
       (case e of
-        Block ((bg, en), bes, indent, wd) =>
+        Block ((bg, en), bes, indent, _) =>
           let
             val {emergencypos, ...} = ! margin_info;
             val pos' = pos + indent;

--- a/src/Pure/General/scan.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/General/scan.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -273,7 +273,7 @@
 val empty_lexicon = Lexicon Symtab.empty;
 
 fun is_literal _ [] = false
-  | is_literal (Lexicon tab) (chs as c :: cs) =
+  | is_literal (Lexicon tab) (c :: cs) =
       (case Symtab.lookup tab c of
         SOME (tip, lex) => tip andalso null cs orelse is_literal lex cs
       | NONE => false);
@@ -286,7 +286,7 @@
     fun finish (SOME (res, rest)) = (rev res, rest)
       | finish NONE = raise FAIL NONE;
     fun scan _ res (Lexicon tab) [] = if Symtab.is_empty tab then finish res else raise MORE NONE
-      | scan path res (Lexicon tab) (chs as c :: cs) =
+      | scan path res (Lexicon tab) (c :: cs) =
           (case Symtab.lookup tab (fst c) of
             SOME (tip, lex) =>
               let val path' = c :: path
@@ -300,7 +300,7 @@
 fun extend_lexicon chrs lexicon =
   let
     fun ext [] lex = lex
-      | ext (chs as c :: cs) (Lexicon tab) =
+      | ext (c :: cs) (Lexicon tab) =
           (case Symtab.lookup tab c of
             SOME (tip, lex) => Lexicon (Symtab.update (c, (tip orelse null cs, ext cs lex)) tab)
           | NONE => Lexicon (Symtab.update (c, (null cs, ext cs empty_lexicon)) tab));

--- a/src/Pure/General/symbol_pos.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/General/symbol_pos.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -161,7 +161,7 @@
 
 fun pad [] = []
   | pad [(s, _)] = [s]
-  | pad ((s1, pos1) :: (rest as (s2, pos2) :: _)) =
+  | pad ((s1, pos1) :: (rest as (_, pos2) :: _)) =
       let
         val end_pos1 = Position.advance s1 pos1;
         val d = Int.max (0, Position.distance_of end_pos1 pos2);

--- a/src/Pure/Isar/args.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/Isar/args.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -283,7 +283,7 @@
 
 (** syntax wrapper **)
 
-fun syntax kind scan (src as Src ((s, args), pos)) st =
+fun syntax kind scan (Src ((s, args), pos)) st =
   (case Scan.error (Scan.finite' T.stopper (Scan.option scan)) (st, args) of
     (SOME x, (st', [])) => (x, st')
   | (_, (_, args')) =>

--- a/src/Pure/Isar/context_rules.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/Isar/context_rules.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -131,8 +131,8 @@
 (* retrieving rules *)
 
 fun untaglist [] = []
-  | untaglist [(k : int * int, x)] = [x]
-  | untaglist ((k, x) :: (rest as (k', x') :: _)) =
+  | untaglist [(_ : int * int, x)] = [x]
+  | untaglist ((k, x) :: (rest as (k', _) :: _)) =
       if k = k' then untaglist rest
       else x :: untaglist rest;
 
@@ -160,7 +160,7 @@
 (* wrappers *)
 
 fun gen_add_wrapper upd w =
-  Context.theory_map (Rules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
+  Context.theory_map (Rules.map (fn Rules {next, rules, netpairs, wrappers} =>
     make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers)));
 
 val addSWrapper = gen_add_wrapper Library.apfst;

--- a/src/Pure/Isar/proof_context.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -1033,7 +1033,7 @@
 
 local
 
-fun const_syntax ctxt (Free (x, T), mx) = SOME (true, (x, T, mx))
+fun const_syntax _ (Free (x, T), mx) = SOME (true, (x, T, mx))
   | const_syntax ctxt (Const (c, _), mx) =
       Option.map (pair false) (try (Consts.syntax (consts_of ctxt)) (c, mx))
   | const_syntax _ _ = NONE;
@@ -1106,7 +1106,7 @@
 
 (* fixes vs. frees *)
 
-fun auto_fixes (arg as (ctxt, (propss, x))) =
+fun auto_fixes (ctxt, (propss, x)) =
   ((fold o fold) Variable.auto_fixes propss ctxt, (propss, x));
 
 fun bind_fixes xs ctxt =

--- a/src/Pure/Isar/proof_node.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/Isar/proof_node.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -41,7 +41,7 @@
 
 (* apply transformer *)
 
-fun applys f (ProofNode (node as (st, _), n)) =
+fun applys f (ProofNode ((st, _), n)) =
   (case Seq.pull (f st) of
     NONE => error "empty result sequence -- proof command failed"
   | SOME res => ProofNode (res, n + 1));

--- a/src/Pure/Isar/rule_insts.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -266,8 +266,8 @@
   let
     val thy = ProofContext.theory_of ctxt;
     (* Separate type and term insts *)
-    fun has_type_var ((x, _), _) = (case Symbol.explode x of
-          "'"::cs => true | cs => false);
+    fun has_type_var ((x, _), _) =
+      (case Symbol.explode x of "'" :: _ => true | _ => false);
     val Tinsts = List.filter has_type_var insts;
     val tinsts = filter_out has_type_var insts;
 

--- a/src/Pure/ML/ml_antiquote.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -41,7 +41,7 @@
     (Context.Proof ctxt, fn {background, ...} => (K ("", ""), background)))));
 
 fun inline name scan = ML_Context.add_antiq name
-  (fn _ => scan >> (fn s => fn {struct_name, background} => (K ("", s), background)));
+  (fn _ => scan >> (fn s => fn {background, ...} => (K ("", s), background)));
 
 fun declaration kind name scan = ML_Context.add_antiq name
   (fn _ => scan >> (fn s => fn {struct_name, background} =>

--- a/src/Pure/Proof/extraction.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/Proof/extraction.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -81,8 +81,7 @@
   {next = next - 1, rs = r :: rs, net = Net.insert_term (K false)
      (Envir.eta_contract lhs, (next, r)) net};
 
-fun merge_rules
-  ({next, rs = rs1, net} : rules) ({next = next2, rs = rs2, ...} : rules) =
+fun merge_rules ({next, rs = rs1, net} : rules) ({rs = rs2, ...} : rules) =
   List.foldr add_rule {next = next, rs = rs1, net = net} (subtract (op =) rs1 rs2);
 
 fun condrew thy rules procs =
@@ -141,7 +140,7 @@
   map_proof_terms (subst_TVars tye) (typ_subst_TVars tye);
 
 fun relevant_vars types prop = List.foldr (fn
-      (Var ((a, i), T), vs) => (case strip_type T of
+      (Var ((a, _), T), vs) => (case strip_type T of
         (_, Type (s, _)) => if member (op =) types s then a :: vs else vs
       | _ => vs)
     | (_, vs) => vs) [] (vars_of prop);

--- a/src/Pure/Syntax/ast.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/Syntax/ast.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -94,7 +94,7 @@
 
 (** check translation rules **)
 
-fun rule_error (rule as (lhs, rhs)) =
+fun rule_error (lhs, rhs) =
   let
     fun add_vars (Constant _) = I
       | add_vars (Variable x) = cons x

--- a/src/Pure/Syntax/syntax.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/Syntax/syntax.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -404,7 +404,7 @@
 
 fun pretty_gram (Syntax (tabs, _)) =
   let
-    val {lexicon, prmodes, gram, prtabs, ...} = tabs;
+    val {lexicon, prmodes, gram, ...} = tabs;
     val prmodes' = sort_strings (filter_out (fn s => s = "") prmodes);
   in
     [pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon),
@@ -639,7 +639,7 @@
 
 local
 
-fun unparse_t t_to_ast prt_t markup ctxt (syn as Syntax (tabs, _)) curried t =
+fun unparse_t t_to_ast prt_t markup ctxt (Syntax (tabs, _)) curried t =
   let
     val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
     val ast = t_to_ast ctxt (lookup_tr' print_trtab) t;

--- a/src/Pure/Syntax/type_ext.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -82,8 +82,8 @@
           if Lexicon.is_tid x then TFree (x, get_sort (x, ~1))
           else Type (x, [])
       | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
-      | typ_of (Const ("_tfree",_) $ (t as Free x)) = typ_of t
-      | typ_of (Const ("_tvar",_) $ (t as Var x)) = typ_of t
+      | typ_of (Const ("_tfree",_) $ (t as Free _)) = typ_of t
+      | typ_of (Const ("_tvar",_) $ (t as Var _)) = typ_of t
       | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1))
       | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) =
           TFree (x, get_sort (x, ~1))

--- a/src/Pure/consts.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/consts.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -199,7 +199,7 @@
 
 fun subscript (Type (_, Ts)) (i :: is) = subscript (nth Ts i) is
   | subscript T [] = T
-  | subscript T _ = raise Subscript;
+  | subscript _ _ = raise Subscript;
 
 in
 

--- a/src/Pure/context.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/context.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -455,7 +455,7 @@
 
 fun init_proof thy = Prf (init_data thy, check_thy thy);
 
-fun transfer_proof thy' (prf as Prf (data, thy_ref)) =
+fun transfer_proof thy' (Prf (data, thy_ref)) =
   let
     val thy = deref thy_ref;
     val _ = subthy (thy, thy') orelse error "transfer proof context: not a super theory";

--- a/src/Pure/display.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/display.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -177,7 +177,7 @@
     val axioms = (Theory.axiom_space thy, Theory.axiom_table thy);
     val defs = Theory.defs_of thy;
     val {restricts, reducts} = Defs.dest defs;
-    val {naming, syn = _, tsig, consts} = Sign.rep_sg thy;
+    val {naming = _, syn = _, tsig, consts} = Sign.rep_sg thy;
     val {constants, constraints} = Consts.dest consts;
     val extern_const = NameSpace.extern (#1 constants);
     val {classes, default, types, ...} = Type.rep_tsig tsig;

--- a/src/Pure/logic.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/logic.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -222,7 +222,7 @@
 fun mk_of_class (ty, c) =
   Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
 
-fun dest_of_class (t as Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
+fun dest_of_class (Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
   | dest_of_class t = raise TERM ("dest_of_class", [t]);
 
 

--- a/src/Pure/term.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/term.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -796,7 +796,7 @@
       let
         fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T)
           | subst (Free (a, T)) = Free (a, typ_subst_TVars instT T)
-          | subst (t as Var (xi, T)) =
+          | subst (Var (xi, T)) =
               (case AList.lookup (op =) inst xi of
                 NONE => Var (xi, typ_subst_TVars instT T)
               | SOME t => t)

--- a/src/Pure/thm.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/thm.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -181,7 +181,7 @@
     val sorts = Sorts.insert_typ T [];
   in Ctyp {thy_ref = Theory.check_thy thy, T = T, maxidx = maxidx, sorts = sorts} end;
 
-fun dest_ctyp (Ctyp {thy_ref, T = Type (s, Ts), maxidx, sorts}) =
+fun dest_ctyp (Ctyp {thy_ref, T = Type (_, Ts), maxidx, sorts}) =
       map (fn T => Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}) Ts
   | dest_ctyp cT = raise TYPE ("dest_ctyp", [typ_of cT], []);
 
@@ -218,31 +218,31 @@
     val sorts = Sorts.insert_term t [];
   in Cterm {thy_ref = Theory.check_thy thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end;
 
-fun merge_thys0 (Cterm {thy_ref = r1, t = t1, ...}) (Cterm {thy_ref = r2, t = t2, ...}) =
+fun merge_thys0 (Cterm {thy_ref = r1, ...}) (Cterm {thy_ref = r2, ...}) =
   Theory.merge_refs (r1, r2);
 
 
 (* destructors *)
 
-fun dest_comb (ct as Cterm {t = c $ a, T, thy_ref, maxidx, sorts}) =
+fun dest_comb (Cterm {t = c $ a, T, thy_ref, maxidx, sorts}) =
       let val A = Term.argument_type_of c 0 in
         (Cterm {t = c, T = A --> T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts},
          Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts})
       end
   | dest_comb ct = raise CTERM ("dest_comb", [ct]);
 
-fun dest_fun (ct as Cterm {t = c $ _, T, thy_ref, maxidx, sorts}) =
+fun dest_fun (Cterm {t = c $ _, T, thy_ref, maxidx, sorts}) =
       let val A = Term.argument_type_of c 0
       in Cterm {t = c, T = A --> T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end
   | dest_fun ct = raise CTERM ("dest_fun", [ct]);
 
-fun dest_arg (ct as Cterm {t = c $ a, T = _, thy_ref, maxidx, sorts}) =
+fun dest_arg (Cterm {t = c $ a, T = _, thy_ref, maxidx, sorts}) =
       let val A = Term.argument_type_of c 0
       in Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end
   | dest_arg ct = raise CTERM ("dest_arg", [ct]);
 
 
-fun dest_fun2 (Cterm {t = c $ a $ b, T, thy_ref, maxidx, sorts}) =
+fun dest_fun2 (Cterm {t = c $ _ $ _, T, thy_ref, maxidx, sorts}) =
       let
         val A = Term.argument_type_of c 0;
         val B = Term.argument_type_of c 1;
@@ -254,8 +254,7 @@
       in Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end
   | dest_arg1 ct = raise CTERM ("dest_arg1", [ct]);
 
-fun dest_abs a (ct as
-        Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), thy_ref, maxidx, sorts}) =
+fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), thy_ref, maxidx, sorts}) =
       let val (y', t') = Term.dest_abs (the_default x a, T, t) in
         (Cterm {t = Free (y', T), T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts},
           Cterm {t = t', T = U, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts})
@@ -392,10 +391,10 @@
 
 (* merge theories of cterms/thms -- trivial absorption only *)
 
-fun merge_thys1 (Cterm {thy_ref = r1, ...}) (th as Thm (_, {thy_ref = r2, ...})) =
+fun merge_thys1 (Cterm {thy_ref = r1, ...}) (Thm (_, {thy_ref = r2, ...})) =
   Theory.merge_refs (r1, r2);
 
-fun merge_thys2 (th1 as Thm (_, {thy_ref = r1, ...})) (th2 as Thm (_, {thy_ref = r2, ...})) =
+fun merge_thys2 (Thm (_, {thy_ref = r1, ...})) (Thm (_, {thy_ref = r2, ...})) =
   Theory.merge_refs (r1, r2);
 
 
@@ -808,7 +807,7 @@
 (*Reflexivity
   t == t
 *)
-fun reflexive (ct as Cterm {thy_ref, t, T, maxidx, sorts}) =
+fun reflexive (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
   Thm (deriv_rule0 Pt.reflexive,
    {thy_ref = thy_ref,
     tags = [],
@@ -825,7 +824,7 @@
 *)
 fun symmetric (th as Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
   (case prop of
-    (eq as Const ("==", Type (_, [T, _]))) $ t $ u =>
+    (eq as Const ("==", _)) $ t $ u =>
       Thm (deriv_rule1 Pt.symmetric der,
        {thy_ref = thy_ref,
         tags = [],
@@ -868,7 +867,7 @@
   (%x. t)(u) == t[u/x]
   fully beta-reduces the term if full = true
 *)
-fun beta_conversion full (Cterm {thy_ref, t, T, maxidx, sorts}) =
+fun beta_conversion full (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
   let val t' =
     if full then Envir.beta_norm t
     else
@@ -885,7 +884,7 @@
       prop = Logic.mk_equals (t, t')})
   end;
 
-fun eta_conversion (Cterm {thy_ref, t, T, maxidx, sorts}) =
+fun eta_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
   Thm (deriv_rule0 Pt.reflexive,
    {thy_ref = thy_ref,
     tags = [],
@@ -895,7 +894,7 @@
     tpairs = [],
     prop = Logic.mk_equals (t, Envir.eta_contract t)});
 
-fun eta_long_conversion (Cterm {thy_ref, t, T, maxidx, sorts}) =
+fun eta_long_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
   Thm (deriv_rule0 Pt.reflexive,
    {thy_ref = thy_ref,
     tags = [],
@@ -951,7 +950,7 @@
       prop = prop2, ...}) = th2;
     fun chktypes fT tT =
       (case fT of
-        Type ("fun", [T1, T2]) =>
+        Type ("fun", [T1, _]) =>
           if T1 <> tT then
             raise THM ("combination: types", 0, [th1, th2])
           else ()
@@ -1264,7 +1263,7 @@
 val varifyT = #2 o varifyT' [];
 
 (* Replace all TVars by new TFrees *)
-fun freezeT (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
+fun freezeT (Thm (der, {thy_ref, shyps, hyps, tpairs, prop, ...})) =
   let
     val prop1 = attach_tpairs tpairs prop;
     val prop2 = Type.freeze prop1;
@@ -1329,7 +1328,7 @@
 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
 fun assumption i state =
   let
-    val Thm (der, {thy_ref, maxidx, shyps, hyps, prop, ...}) = state;
+    val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state;
     val thy = Theory.deref thy_ref;
     val (tpairs, Bs, Bi, C) = dest_state (state, i);
     fun newth n (env, tpairs) =
@@ -1365,7 +1364,7 @@
   Checks if Bi's conclusion is alpha-convertible to one of its assumptions*)
 fun eq_assumption i state =
   let
-    val Thm (der, {thy_ref, maxidx, shyps, hyps, prop, ...}) = state;
+    val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state;
     val (tpairs, Bs, Bi, C) = dest_state (state, i);
     val (_, asms, concl) = Logic.assum_problems (~1, Bi);
   in
@@ -1386,7 +1385,7 @@
 (*For rotate_tac: fast rotation of assumptions of subgoal i*)
 fun rotate_rule k i state =
   let
-    val Thm (der, {thy_ref, maxidx, shyps, hyps, prop, ...}) = state;
+    val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state;
     val (tpairs, Bs, Bi, C) = dest_state (state, i);
     val params = Term.strip_all_vars Bi
     and rest   = Term.strip_all_body Bi;
@@ -1558,7 +1557,7 @@
       in Term.all T' $ Abs (a, T', norm_term_skip env n t) end
   | norm_term_skip env n (Const ("==>", _) $ A $ B) =
       Logic.mk_implies (A, norm_term_skip env (n - 1) B)
-  | norm_term_skip env n t = error "norm_term_skip: too few assumptions??";
+  | norm_term_skip _ _ _ = error "norm_term_skip: too few assumptions??";
 
 
 (*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C)

--- a/src/Pure/type.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/type.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -140,7 +140,7 @@
 fun cert_class (TSig {classes, ...}) = Sorts.certify_class (#2 classes);
 fun cert_sort (TSig {classes, ...}) = Sorts.certify_sort (#2 classes);
 
-fun witness_sorts (tsig as TSig {classes, log_types, ...}) =
+fun witness_sorts (TSig {classes, log_types, ...}) =
   Sorts.witness_sorts (#2 classes) log_types;
 
 
@@ -280,7 +280,7 @@
     val used = Name.context
       |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
     val fmap = fs ~~ map (rpair 0) (#1 (Name.variants (map fst fs) used));
-    fun thaw (f as (a, S)) =
+    fun thaw (f as (_, S)) =
       (case AList.lookup (op =) fmap f of
         NONE => TFree f
       | SOME xi => TVar (xi, S));
@@ -412,10 +412,10 @@
       (case lookup tye v of
         SOME U => devar tye U
       | NONE => T)
-  | devar tye T = T;
+  | devar _ T = T;
 
 (*order-sorted unification*)
-fun unify (tsig as TSig {classes = (_, classes), ...}) TU (tyenv, maxidx) =
+fun unify (TSig {classes = (_, classes), ...}) TU (tyenv, maxidx) =
   let
     val tyvar_count = Unsynchronized.ref maxidx;
     fun gen_tyvar S = TVar ((Name.aT, Unsynchronized.inc tyvar_count), S);
@@ -465,7 +465,7 @@
 (*purely structural unification*)
 fun raw_unify (ty1, ty2) tye =
   (case (devar tye ty1, devar tye ty2) of
-    (T as TVar (v, S1), U as TVar (w, S2)) =>
+    (T as TVar (v, S1), TVar (w, S2)) =>
       if Term.eq_ix (v, w) then
         if S1 = S2 then tye else tvar_clash v S1 S2
       else Vartab.update_new (w, (S2, T)) tye
@@ -545,7 +545,7 @@
     let
       val rel' = pairself (cert_class tsig) rel
         handle TYPE (msg, _, _) => error msg;
-      val classes' = classes |> Sorts.add_classrel pp rel;
+      val classes' = classes |> Sorts.add_classrel pp rel';
     in ((space, classes'), default, types) end);
 
 

--- a/src/Pure/variable.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/variable.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -89,7 +89,7 @@
 structure Data = ProofDataFun
 (
   type T = data;
-  fun init thy =
+  fun init _ =
     make_data (false, Name.context, Symtab.empty, [], Vartab.empty, Symtab.empty,
       ~1, [], (Vartab.empty, Vartab.empty));
 );