merged
authornipkow
Thu, 01 Oct 2009 15:19:49 +0200
changeset 32820 02f412281b99
parent 32809 e72347dd3e64 (diff)
parent 32819 004b251ac927 (current diff)
child 32821 99843bbfaeb2
child 32822 45fa9254ddc8
child 32824 712ad8109fff
merged
--- a/src/HOL/Record.thy	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/HOL/Record.thy	Thu Oct 01 15:19:49 2009 +0200
@@ -450,10 +450,6 @@
   "Q = R \<Longrightarrow> (P \<and> Q) = (P \<and> R)"
   by simp
 
-lemma meta_all_sameI:
-  "(\<And>x. PROP P x \<equiv> PROP Q x) \<Longrightarrow> (\<And>x. PROP P x) \<equiv> (\<And>x. PROP Q x)"
-  by simp
-
 lemma istuple_UNIV_I: "\<And>x. x\<in>UNIV \<equiv> True"
   by simp
 
--- a/src/HOL/Tools/record.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/HOL/Tools/record.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -202,22 +202,18 @@
 struct
 
 val eq_reflection = @{thm eq_reflection};
-val Pair_eq = @{thm Product_Type.prod.inject};
 val atomize_all = @{thm HOL.atomize_all};
 val atomize_imp = @{thm HOL.atomize_imp};
 val meta_allE = @{thm Pure.meta_allE};
 val prop_subst = @{thm prop_subst};
-val Pair_sel_convs = [fst_conv, snd_conv];
 val K_record_comp = @{thm K_record_comp};
 val K_comp_convs = [@{thm o_apply}, K_record_comp]
-val transitive_thm = @{thm transitive};
 val o_assoc = @{thm o_assoc};
 val id_apply = @{thm id_apply};
 val id_o_apps = [@{thm id_apply}, @{thm id_o}, @{thm o_id}];
 val Not_eq_iff = @{thm Not_eq_iff};
 
 val refl_conj_eq = @{thm refl_conj_eq};
-val meta_all_sameI = @{thm meta_all_sameI};
 
 val surject_assistI = @{thm "istuple_surjective_proof_assistI"};
 val surject_assist_idE = @{thm "istuple_surjective_proof_assist_idE"};
@@ -250,7 +246,6 @@
 val ext_typeN = "_ext_type";
 val inner_typeN = "_inner_type";
 val extN ="_ext";
-val casesN = "_cases";
 val ext_dest = "_sel";
 val updateN = "_update";
 val updN = "_upd";
@@ -259,10 +254,6 @@
 val extendN = "extend";
 val truncateN = "truncate";
 
-(*see typedef.ML*)
-val RepN = "Rep_";
-val AbsN = "Abs_";
-
 
 
 (*** utilities ***)
@@ -273,24 +264,6 @@
   let fun varify (a, S) = TVar ((a, midx + 1), S);
   in map_type_tfree varify end;
 
-fun domain_type' T =
-  domain_type T handle Match => T;
-
-fun range_type' T =
-  range_type T handle Match => T;
-
-
-(* messages *)  (* FIXME proper context *)
-
-fun trace_thm str thm =
-  tracing (str ^ Pretty.string_of (Display.pretty_thm_without_context thm));
-
-fun trace_thms str thms =
-  (tracing str; map (trace_thm "") thms);
-
-fun trace_term str t =
-  tracing (str ^ Syntax.string_of_term_global Pure.thy t);
-
 
 (* timing *)
 
@@ -302,7 +275,6 @@
 (* syntax *)
 
 fun prune n xs = Library.drop (n, xs);
-fun prefix_base s = Long_Name.map_base_name (fn bname => s ^ bname);
 
 val Trueprop = HOLogic.mk_Trueprop;
 fun All xs t = Term.list_all_free (xs, t);
@@ -311,22 +283,10 @@
 infix 0 :== ===;
 infixr 0 ==>;
 
-val (op $$) = Term.list_comb;
-val (op :==) = PrimitiveDefs.mk_defpair;
-val (op ===) = Trueprop o HOLogic.mk_eq;
-val (op ==>) = Logic.mk_implies;
-
-
-(* morphisms *)
-
-fun mk_RepN name = suffix ext_typeN (prefix_base RepN name);
-fun mk_AbsN name = suffix ext_typeN (prefix_base AbsN name);
-
-fun mk_Rep name repT absT =
-  Const (suffix ext_typeN (prefix_base RepN name), absT --> repT);
-
-fun mk_Abs name repT absT =
-  Const (mk_AbsN name, repT --> absT);
+val op $$ = Term.list_comb;
+val op :== = PrimitiveDefs.mk_defpair;
+val op === = Trueprop o HOLogic.mk_eq;
+val op ==> = Logic.mk_implies;
 
 
 (* constructor *)
@@ -338,15 +298,6 @@
   in list_comb (Const (mk_extC (name, T) Ts), ts) end;
 
 
-(* cases *)
-
-fun mk_casesC (name, T, vT) Ts = (suffix casesN name, (Ts ---> vT) --> T --> vT);
-
-fun mk_cases (name, T, vT) f =
-  let val Ts = binder_types (fastype_of f)
-  in Const (mk_casesC (name, T, vT) Ts) $ f end;
-
-
 (* selector *)
 
 fun mk_selC sT (c, T) = (c, sT --> T);
@@ -369,7 +320,7 @@
 
 (* types *)
 
-fun dest_recT (typ as Type (c_ext_type, Ts as (T :: _))) =
+fun dest_recT (typ as Type (c_ext_type, Ts as (_ :: _))) =
       (case try (unsuffix ext_typeN) c_ext_type of
         NONE => raise TYPE ("Record.dest_recT", [typ], [])
       | SOME c => ((c, Ts), List.last Ts))
@@ -549,8 +500,6 @@
 
 val get_simpset = get_ss_with_context #simpset;
 val get_sel_upd_defs = get_ss_with_context #defset;
-val get_foldcong_ss = get_ss_with_context #foldcong;
-val get_unfoldcong_ss = get_ss_with_context #unfoldcong;
 
 fun get_update_details u thy =
   let val sel_upd = get_sel_upd thy in
@@ -618,8 +567,6 @@
       extfields fieldext;
   in RecordsData.put data thy end;
 
-val get_extsplit = Symtab.lookup o #extsplit o RecordsData.get;
-
 
 (* access 'splits' *)
 
@@ -659,7 +606,7 @@
   let
     val ((name, Ts), moreT) = dest_recT T;
     val recname =
-      let val (nm :: recn :: rst) = rev (Long_Name.explode name)
+      let val (nm :: _ :: rst) = rev (Long_Name.explode name)   (* FIXME !? *)
       in Long_Name.implode (rev (nm :: rst)) end;
     val midx = maxidx_of_typs (moreT :: Ts);
     val varifyT = varifyT midx;
@@ -698,7 +645,7 @@
 
 (* parent records *)
 
-fun add_parents thy NONE parents = parents
+fun add_parents _ NONE parents = parents
   | add_parents thy (SOME (types, name)) parents =
       let
         fun err msg = error (msg ^ " parent record " ^ quote name);
@@ -787,7 +734,7 @@
       | splitargs (_ :: _) [] = raise TERM (msg ^ "expecting more fields", [t])
       | splitargs _ _ = ([], []);
 
-    fun mk_ext (fargs as (name, arg) :: _) =
+    fun mk_ext (fargs as (name, _) :: _) =
           (case get_fieldext thy (Sign.intern_const thy name) of
             SOME (ext, _) =>
               (case get_extfields thy ext of
@@ -816,7 +763,7 @@
       | splitargs (_ :: _) [] = raise TERM (msg ^ "expecting more fields", [t])
       | splitargs _ _ = ([], []);
 
-    fun mk_ext (fargs as (name, arg) :: _) =
+    fun mk_ext (fargs as (name, _) :: _) =
           (case get_fieldext thy (Sign.intern_const thy name) of
             SOME (ext, alphas) =>
               (case get_extfields thy ext of
@@ -838,7 +785,7 @@
                     val more' = mk_ext rest;
                   in
                     list_comb (Syntax.const (suffix sfx ext), alphas' @ [more'])
-                  end handle TYPE_MATCH =>
+                  end handle Type.TYPE_MATCH =>
                     raise TERM (msg ^ "type is no proper record (extension)", [t]))
               | NONE => raise TERM (msg ^ "no fields defined for " ^ ext, [t]))
           | NONE => raise TERM (msg ^ name ^" is no proper field", [t]))
@@ -896,7 +843,7 @@
           (case k of
             Abs (_, _, Abs (_, _, t) $ Bound 0) =>
               if null (loose_bnos t) then t else raise Match
-          | Abs (x, _, t) =>
+          | Abs (_, _, t) =>
               if null (loose_bnos t) then t else raise Match
           | _ => raise Match);
 
@@ -1012,7 +959,7 @@
               if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree (zeta, Sign.defaultS thy))))
               then mk_type_abbr subst abbr alphas
               else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
-            end handle TYPE_MATCH => default_tr' ctxt tm)
+            end handle Type.TYPE_MATCH => default_tr' ctxt tm)
           else raise Match (*give print translation of specialised record a chance*)
       | _ => raise Match)
     else default_tr' ctxt tm
@@ -1045,8 +992,7 @@
                         val subst = fold2 (curry (Sign.typ_match thy)) alphavars args' Vartab.empty;
                         val flds'' = (map o apsnd) (Envir.norm_type subst o varifyT) flds';
                       in flds'' @ field_lst more end
-                      handle TYPE_MATCH => [("", T)]
-                        | Library.UnequalLengths => [("", T)])
+                      handle Type.TYPE_MATCH => [("", T)] | Library.UnequalLengths => [("", T)])
                   | NONE => [("", T)])
               | NONE => [("", T)])
           | NONE => [("", T)])
@@ -1106,7 +1052,7 @@
   then noopt ()
   else opt ();
 
-fun is_sel_upd_pair thy (Const (s, t)) (Const (u, t')) =
+fun is_sel_upd_pair thy (Const (s, _)) (Const (u, t')) =
   (case get_updates thy u of
     SOME u_name => u_name = s
   | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]));
@@ -1130,7 +1076,6 @@
 fun get_accupd_simps thy term defset intros_tac =
   let
     val (acc, [body]) = strip_comb term;
-    val recT = domain_type (fastype_of acc);
     val upd_funs = sort_distinct TermOrd.fast_term_ord (get_upd_funs body);
     fun get_simp upd =
       let
@@ -1140,10 +1085,10 @@
           if is_sel_upd_pair thy acc upd
           then mk_comp (Free ("f", T)) acc
           else mk_comp_id acc;
-        val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
+        val prop = lhs === rhs;
         val othm =
           Goal.prove (ProofContext.init thy) [] [] prop
-            (fn prems =>
+            (fn _ =>
               EVERY
                [simp_tac defset 1,
                 REPEAT_DETERM (intros_tac 1),
@@ -1164,10 +1109,10 @@
       if comp
       then u $ mk_comp f f'
       else mk_comp (u' $ f') (u $ f);
-    val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
+    val prop = lhs === rhs;
     val othm =
       Goal.prove (ProofContext.init thy) [] [] prop
-        (fn prems =>
+        (fn _ =>
           EVERY
            [simp_tac defset 1,
             REPEAT_DETERM (intros_tac 1),
@@ -1177,11 +1122,10 @@
 
 fun get_updupd_simps thy term defset intros_tac =
   let
-    val recT = fastype_of term;
     val upd_funs = get_upd_funs term;
     val cname = fst o dest_Const;
     fun getswap u u' = get_updupd_simp thy defset intros_tac u u' (cname u = cname u');
-    fun build_swaps_to_eq upd [] swaps = swaps
+    fun build_swaps_to_eq _ [] swaps = swaps
       | build_swaps_to_eq upd (u :: us) swaps =
           let
             val key = (cname u, cname upd);
@@ -1192,7 +1136,7 @@
             if cname u = cname upd then newswaps
             else build_swaps_to_eq upd us newswaps
           end;
-    fun swaps_needed [] prev seen swaps = map snd (Symreltab.dest swaps)
+    fun swaps_needed [] _ _ swaps = map snd (Symreltab.dest swaps)
       | swaps_needed (u :: us) prev seen swaps =
           if Symtab.defined seen (cname u)
           then swaps_needed us prev seen (build_swaps_to_eq u prev swaps)
@@ -1201,20 +1145,20 @@
 
 val named_cterm_instantiate = IsTupleSupport.named_cterm_instantiate;
 
-fun prove_unfold_defs thy ss T ex_simps ex_simprs prop =
+fun prove_unfold_defs thy ex_simps ex_simprs prop =
   let
     val defset = get_sel_upd_defs thy;
     val in_tac = IsTupleSupport.istuple_intros_tac thy;
     val prop' = Envir.beta_eta_contract prop;
-    val (lhs, rhs) = Logic.dest_equals (Logic.strip_assums_concl prop');
-    val (head, args) = strip_comb lhs;
+    val (lhs, _) = Logic.dest_equals (Logic.strip_assums_concl prop');
+    val (_, args) = strip_comb lhs;
     val simps =
       if length args = 1
       then get_accupd_simps thy lhs defset in_tac
       else get_updupd_simps thy lhs defset in_tac;
   in
     Goal.prove (ProofContext.init thy) [] [] prop'
-      (fn prems =>
+      (fn _ =>
         simp_tac (HOL_basic_ss addsimps (simps @ [K_record_comp])) 1 THEN
         TRY (simp_tac (HOL_basic_ss addsimps ex_simps addsimprocs ex_simprs) 1))
   end;
@@ -1251,55 +1195,52 @@
 *)
 val record_simproc =
   Simplifier.simproc @{theory HOL} "record_simp" ["x"]
-    (fn thy => fn ss => fn t =>
+    (fn thy => fn _ => fn t =>
       (case t of
-        (sel as Const (s, Type (_, [domS, rangeS]))) $
+        (sel as Const (s, Type (_, [_, rangeS]))) $
             ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) =>
-          if is_selector thy s then
-            (case get_updates thy u of
-              SOME u_name =>
-                let
-                  val {sel_upd = {updates, ...}, extfields, ...} = RecordsData.get thy;
-
-                  fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) =
-                        (case Symtab.lookup updates u of
-                          NONE => NONE
-                        | SOME u_name =>
-                            if u_name = s then
-                              (case mk_eq_terms r of
-                                NONE =>
-                                  let
-                                    val rv = ("r", rT);
-                                    val rb = Bound 0;
-                                    val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
-                                  in SOME (upd $ kb $ rb, kb $ (sel $ rb), [kv, rv]) end
-                              | SOME (trm, trm', vars) =>
-                                  let
-                                    val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k;
-                                  in SOME (upd $ kb $ trm, kb $ trm', kv :: vars) end)
-                            else if has_field extfields u_name rangeS orelse
-                              has_field extfields s (domain_type kT) then NONE
-                            else
-                              (case mk_eq_terms r of
-                                SOME (trm, trm', vars) =>
-                                  let val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k
-                                  in SOME (upd $ kb $ trm, trm', kv :: vars) end
-                              | NONE =>
-                                  let
-                                    val rv = ("r", rT);
-                                    val rb = Bound 0;
-                                    val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
-                                  in SOME (upd $ kb $ rb, sel $ rb, [kv, rv]) end))
-                    | mk_eq_terms r = NONE;
-                in
-                  (case mk_eq_terms (upd $ k $ r) of
-                    SOME (trm, trm', vars) =>
-                      SOME
-                        (prove_unfold_defs thy ss domS [] []
-                          (list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
-                  | NONE => NONE)
-                end
-            | NONE => NONE)
+          if is_selector thy s andalso is_some (get_updates thy u) then
+            let
+              val {sel_upd = {updates, ...}, extfields, ...} = RecordsData.get thy;
+
+              fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) =
+                    (case Symtab.lookup updates u of
+                      NONE => NONE
+                    | SOME u_name =>
+                        if u_name = s then
+                          (case mk_eq_terms r of
+                            NONE =>
+                              let
+                                val rv = ("r", rT);
+                                val rb = Bound 0;
+                                val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
+                              in SOME (upd $ kb $ rb, kb $ (sel $ rb), [kv, rv]) end
+                          | SOME (trm, trm', vars) =>
+                              let
+                                val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k;
+                              in SOME (upd $ kb $ trm, kb $ trm', kv :: vars) end)
+                        else if has_field extfields u_name rangeS orelse
+                          has_field extfields s (domain_type kT) then NONE
+                        else
+                          (case mk_eq_terms r of
+                            SOME (trm, trm', vars) =>
+                              let val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k
+                              in SOME (upd $ kb $ trm, trm', kv :: vars) end
+                          | NONE =>
+                              let
+                                val rv = ("r", rT);
+                                val rb = Bound 0;
+                                val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
+                              in SOME (upd $ kb $ rb, sel $ rb, [kv, rv]) end))
+                | mk_eq_terms _ = NONE;
+            in
+              (case mk_eq_terms (upd $ k $ r) of
+                SOME (trm, trm', vars) =>
+                  SOME
+                    (prove_unfold_defs thy [] []
+                      (list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
+              | NONE => NONE)
+            end
           else NONE
       | _ => NONE));
 
@@ -1311,7 +1252,7 @@
     val prop = concl_of (named_cterm_instantiate insts updacc_cong_triv);
   in
     Goal.prove (ProofContext.init thy) [] [] prop
-      (fn prems =>
+      (fn _ =>
         EVERY
          [simp_tac simpset 1,
           REPEAT_DETERM (in_tac 1),
@@ -1331,7 +1272,7 @@
   both a more update and an update to a field within it.*)
 val record_upd_simproc =
   Simplifier.simproc @{theory HOL} "record_upd_simp" ["x"]
-    (fn thy => fn ss => fn t =>
+    (fn thy => fn _ => fn t =>
       let
         (*We can use more-updators with other updators as long
           as none of the other updators go deeper than any more
@@ -1346,7 +1287,7 @@
               then SOME (if min <= dep then dep else min, max)
               else NONE;
 
-        fun getupdseq (term as (upd as Const (u, T)) $ f $ tm) min max =
+        fun getupdseq (term as (upd as Const (u, _)) $ f $ tm) min max =
               (case get_update_details u thy of
                 SOME (s, dep, ismore) =>
                   (case include_depth (dep, ismore) (min, max) of
@@ -1359,15 +1300,14 @@
 
         val (upds, base, baseT) = getupdseq t 0 ~1;
 
-        fun is_upd_noop s (f as Abs (n, T, Const (s', T') $ tm')) tm =
+        fun is_upd_noop s (Abs (n, T, Const (s', T') $ tm')) tm =
               if s = s' andalso null (loose_bnos tm')
                 andalso subst_bound (HOLogic.unit, tm') = tm
               then (true, Abs (n, T, Const (s', T') $ Bound 1))
               else (false, HOLogic.unit)
-          | is_upd_noop s f tm = (false, HOLogic.unit);
-
-        fun get_noop_simps (upd as Const (u, T))
-            (f as Abs (n, T', (acc as Const (s, T'')) $ _)) =
+          | is_upd_noop _ _ _ = (false, HOLogic.unit);
+
+        fun get_noop_simps (upd as Const _) (Abs (_, _, (acc as Const _) $ _)) =
           let
             val ss = get_sel_upd_defs thy;
             val uathm = get_upd_acc_cong_thm upd acc thy ss;
@@ -1417,17 +1357,16 @@
                       fvar :: vars, dups, true, noops)
                   | NONE => (upd $ skelf $ lhs, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops))
               end
-          | mk_updterm [] above term =
+          | mk_updterm [] _ _ =
               (Bound 0, Bound 0, [("r", baseT)], Symtab.empty, false, Symtab.empty)
-          | mk_updterm us above term =
-              raise TERM ("mk_updterm match", map (fn (x, y, z) => x) us);
-
-        val (lhs, rhs, vars, dups, simp, noops) = mk_updterm upds Symtab.empty base;
+          | mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _) => x) us);
+
+        val (lhs, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base;
         val noops' = flat (map snd (Symtab.dest noops));
       in
         if simp then
           SOME
-            (prove_unfold_defs thy ss baseT noops' [record_simproc]
+            (prove_unfold_defs thy noops' [record_simproc]
               (list_all (vars, Logic.mk_equals (lhs, rhs))))
         else NONE
       end);
@@ -1473,11 +1412,11 @@
   Simplifier.simproc @{theory HOL} "record_split_simp" ["x"]
     (fn thy => fn _ => fn t =>
       (case t of
-        Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ trm =>
+        Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
           if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex" then
             (case rec_id ~1 T of
               "" => NONE
-            | name =>
+            | _ =>
                 let val split = P t in
                   if split <> 0 then
                     (case get_splits thy (rec_id split T) of
@@ -1568,10 +1507,10 @@
           simp_tac (HOL_basic_ss addsimps @{thms induct_rulify}) i]
       end;
 
-    fun split_free_tac P i (free as Free (n, T)) =
+    fun split_free_tac P i (free as Free (_, T)) =
           (case rec_id ~1 T of
             "" => NONE
-          | name =>
+          | _ =>
               let val split = P free in
                 if split <> 0 then
                   (case get_splits thy (rec_id split T) of
@@ -1598,8 +1537,6 @@
 (*Split all records in the goal, which are quantified by ! or !!.*)
 fun record_split_tac i st =
   let
-    val thy = Thm.theory_of_thm st;
-
     val has_rec = exists_Const
       (fn (s, Type (_, [Type (_, [T, _]), _])) =>
           (s = "all" orelse s = "All") andalso is_recT T
@@ -1695,40 +1632,16 @@
   in compose_tac (false, rule'', nprems_of rule) i st end;
 
 
-(*!!x1 ... xn. ... ==> EX x1 ... xn. P x1 ... xn;
-  instantiates x1 ... xn with parameters x1 ... xn*)
-fun ex_inst_tac i st =
-  let
-    val thy = Thm.theory_of_thm st;
-    val g = nth (prems_of st) (i - 1);   (* FIXME SUBGOAL *)
-    val params = Logic.strip_params g;
-    val exI' = Thm.lift_rule (Thm.cprem_of st i) exI;
-    val _ $ (_ $ x) = Logic.strip_assums_concl (hd (prems_of exI'));
-    val cx = cterm_of thy (fst (strip_comb x));
-  in
-    Seq.single (Library.foldl (fn (st, v) =>
-      Seq.hd
-        (compose_tac
-          (false,
-            cterm_instantiate [(cx, cterm_of thy (list_abs (params, Bound v)))] exI', 1) i st))
-        (st, (length params - 1) downto 0))
-  end;
-
-fun extension_definition full name fields names alphas zeta moreT more vars thy =
+fun extension_definition name fields alphas zeta moreT more vars thy =
   let
     val base = Long_Name.base_name;
     val fieldTs = (map snd fields);
     val alphas_zeta = alphas @ [zeta];
     val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) alphas_zeta;
-    val vT = TFree (Name.variant alphas_zeta "'v", HOLogic.typeS);
     val extT_name = suffix ext_typeN name
     val extT = Type (extT_name, alphas_zetaTs);
-    val fields_more = fields @ [(full moreN, moreT)];
     val fields_moreTs = fieldTs @ [moreT];
-    val bfields_more = map (apfst base) fields_more;
-    val r = Free (rN, extT);
-    val len = length fields;
-    val idxms = 0 upto len;
+
 
     (*before doing anything else, create the tree of new types
       that will back the record extension*)
@@ -1739,7 +1652,7 @@
       let
         val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
         val nm = suffix suff (Long_Name.base_name name);
-        val (isom, cons, thy') =
+        val (_, cons, thy') =
           IsTupleSupport.add_istuple_type
             (nm, alphas_zeta) (fastype_of left, fastype_of right) thy;
       in
@@ -1763,7 +1676,7 @@
             build_meta_tree_type i' thy' composites more
           end
         else
-          let val (term, (thy', i')) = mk_istuple (mktreeV vars, more) (thy, 0)
+          let val (term, (thy', _)) = mk_istuple (mktreeV vars, more) (thy, 0)
           in (term, thy') end
       end;
 
@@ -1795,16 +1708,15 @@
     val ([ext_def], defs_thy) =
       timeit_msg "record extension constructor def:" mk_defs;
 
+
     (* prepare propositions *)
+
     val _ = timing_msg "record extension preparing propositions";
     val vars_more = vars @ [more];
-    val named_vars_more = (names @ [full moreN]) ~~ vars_more;
     val variants = map (fn Free (x, _) => x) vars_more;
     val ext = mk_ext vars_more;
     val s = Free (rN, extT);
-    val w = Free (wN, extT);
     val P = Free (Name.variant variants "P", extT --> HOLogic.boolT);
-    val C = Free (Name.variant variants "C", HOLogic.boolT);
     val intros_tac = IsTupleSupport.istuple_intros_tac defs_thy;
 
     val inject_prop =
@@ -1819,27 +1731,18 @@
     val induct_prop =
       (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
 
-    val cases_prop =
-      All (map dest_Free vars_more)
-        (Trueprop (HOLogic.mk_eq (s, ext)) ==> Trueprop C)
-      ==> Trueprop C;
-
     val split_meta_prop =
-      let val P = Free (Name.variant variants "P", extT-->Term.propT) in
+      let val P = Free (Name.variant variants "P", extT --> Term.propT) in
         Logic.mk_equals
          (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
       end;
 
-    fun prove stndrd = quick_and_dirty_prove stndrd defs_thy;
     val prove_standard = quick_and_dirty_prove true defs_thy;
-    fun prove_simp stndrd simps =
-      let val tac = simp_all_tac HOL_ss simps
-      in fn prop => prove stndrd [] prop (K tac) end;
 
     fun inject_prf () =
       simplify HOL_ss
         (prove_standard [] inject_prop
-          (fn prems =>
+          (fn _ =>
             EVERY
              [simp_tac (HOL_basic_ss addsimps [ext_def]) 1,
               REPEAT_DETERM (resolve_tac [refl_conj_eq] 1 ORELSE
@@ -1872,7 +1775,7 @@
 
     fun split_meta_prf () =
       prove_standard [] split_meta_prop
-        (fn prems =>
+        (fn _ =>
           EVERY
            [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
             etac meta_allE 1, atac 1,
@@ -1909,8 +1812,8 @@
   | chop_last [x] = ([], x)
   | chop_last (x :: xs) = let val (tl, l) = chop_last xs in (x :: tl, l) end;
 
-fun subst_last s [] = error "subst_last: list should not be empty"
-  | subst_last s [x] = [s]
+fun subst_last _ [] = error "subst_last: list should not be empty"
+  | subst_last s [_] = [s]
   | subst_last s (x :: xs) = x :: subst_last s xs;
 
 
@@ -1965,7 +1868,6 @@
     val parent_variants = Name.variant_list [moreN, rN, rN ^ "'", wN] (map base parent_names);
     val parent_vars = ListPair.map Free (parent_variants, parent_types);
     val parent_len = length parents;
-    val parents_idx = (map #name parents) ~~ (0 upto (parent_len - 1));
 
     val fields = map (apfst full) bfields;
     val names = map fst fields;
@@ -1979,13 +1881,10 @@
         (map fst bfields);
     val vars = ListPair.map Free (variants, types);
     val named_vars = names ~~ vars;
-    val idxs = 0 upto (len - 1);
     val idxms = 0 upto len;
 
     val all_fields = parent_fields @ fields;
-    val all_names = parent_names @ names;
     val all_types = parent_types @ types;
-    val all_len = parent_fields_len + len;
     val all_variants = parent_variants @ variants;
     val all_vars = parent_vars @ vars;
     val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
@@ -1997,7 +1896,6 @@
     val full_moreN = full moreN;
     val bfields_more = bfields @ [(moreN, moreT)];
     val fields_more = fields @ [(full_moreN, moreT)];
-    val vars_more = vars @ [more];
     val named_vars_more = named_vars @ [(full_moreN, more)];
     val all_vars_more = all_vars @ [more];
     val all_named_vars_more = all_named_vars @ [(full_moreN, more)];
@@ -2008,7 +1906,7 @@
     val (extension_thy, extT, ext_induct, ext_inject, ext_split, ext_def) =
       thy
       |> Sign.add_path bname
-      |> extension_definition full extN fields names alphas_ext zeta moreT more vars;
+      |> extension_definition extN fields alphas_ext zeta moreT more vars;
 
     val _ = timing_msg "record preparing definitions";
     val Type extension_scheme = extT;
@@ -2080,16 +1978,6 @@
 
     (* prepare definitions *)
 
-    fun parent_more s =
-      if null parents then s
-      else mk_sel s (Long_Name.qualify (#name (List.last parents)) moreN, extT);
-
-    fun parent_more_upd v s =
-      if null parents then v $ s
-      else
-        let val mp = Long_Name.qualify (#name (List.last parents)) moreN;
-        in mk_upd updateN mp v s end;
-
     (*record (scheme) type abbreviation*)
     val recordT_specs =
       [(Binding.name (suffix schemeN bname), alphas @ [zeta], rec_schemeT0, Syntax.NoSyn),
@@ -2233,14 +2121,12 @@
 
     (*cases*)
     val cases_scheme_prop =
-      (All (map dest_Free all_vars_more)
-        (Trueprop (HOLogic.mk_eq (r0, r_rec0)) ==> Trueprop C))
-      ==> Trueprop C;
+      (All (map dest_Free all_vars_more) ((r0 === r_rec0) ==> Trueprop C))
+        ==> Trueprop C;
 
     val cases_prop =
-      (All (map dest_Free all_vars)
-        (Trueprop (HOLogic.mk_eq (r_unit0, r_rec_unit0)) ==> Trueprop C))
-       ==> Trueprop C;
+      (All (map dest_Free all_vars) ((r_unit0 === r_rec_unit0) ==> Trueprop C))
+         ==> Trueprop C;
 
     (*split*)
     val split_meta_prop =
@@ -2359,7 +2245,7 @@
         val init_ss = HOL_basic_ss addsimps ext_defs;
       in
         prove_standard [] surjective_prop
-          (fn prems =>
+          (fn _ =>
             EVERY
              [rtac surject_assist_idE 1,
               simp_tac init_ss 1,
@@ -2369,7 +2255,7 @@
 
     fun split_meta_prf () =
       prove false [] split_meta_prop
-        (fn prems =>
+        (fn _ =>
           EVERY
            [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
             etac meta_allE 1, atac 1,
@@ -2423,7 +2309,7 @@
         val so' = named_cterm_instantiate ([(P_nm, not_P)]) split_object;
         val so'' = simplify ss so';
       in
-        prove_standard [] split_ex_prop (fn prems => resolve_tac [so''] 1)
+        prove_standard [] split_ex_prop (fn _ => resolve_tac [so''] 1)
       end;
     val split_ex = timeit_msg "record split_ex proof:" split_ex_prf;
 
--- a/src/Pure/Concurrent/task_queue.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Thu Oct 01 15:19:49 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	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/General/heap.ML	Thu Oct 01 15:19:49 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	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/General/pretty.ML	Thu Oct 01 15:19:49 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	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/General/scan.ML	Thu Oct 01 15:19:49 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	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/General/symbol_pos.ML	Thu Oct 01 15:19:49 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	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Isar/args.ML	Thu Oct 01 15:19:49 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	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Isar/context_rules.ML	Thu Oct 01 15:19:49 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/expression.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Isar/expression.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -311,7 +311,7 @@
   | finish_primitive _ close (Defines defs) = close (Defines defs)
   | finish_primitive _ _ (Notes facts) = Notes facts;
 
-fun finish_inst ctxt parms do_close (loc, (prfx, inst)) =
+fun finish_inst ctxt (loc, (prfx, inst)) =
   let
     val thy = ProofContext.theory_of ctxt;
     val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
@@ -323,7 +323,7 @@
 
 fun finish ctxt parms do_close insts elems =
   let
-    val deps = map (finish_inst ctxt parms do_close) insts;
+    val deps = map (finish_inst ctxt) insts;
     val elems' = map (finish_elem ctxt parms do_close) elems;
   in (deps, elems') end;
 
--- a/src/Pure/Isar/isar_document.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Isar/isar_document.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -13,6 +13,7 @@
   val begin_document: document_id -> Path.T -> unit
   val end_document: document_id -> unit
   val edit_document: document_id -> document_id -> (command_id * command_id option) list -> unit
+  val init: unit -> unit
 end;
 
 structure Isar_Document: ISAR_DOCUMENT =
--- a/src/Pure/Isar/obtain.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Isar/obtain.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -215,7 +215,6 @@
     val thy = ProofContext.theory_of ctxt;
     val certT = Thm.ctyp_of thy;
     val cert = Thm.cterm_of thy;
-    val string_of_typ = Syntax.string_of_typ ctxt;
     val string_of_term = setmp show_types true (Syntax.string_of_term ctxt);
 
     fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th);
--- a/src/Pure/Isar/proof.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -581,7 +581,6 @@
   let
     val _ = assert_forward state;
     val thy = theory_of state;
-    val ctxt = context_of state;
 
     val (raw_name_atts, (raw_vars, raw_rhss)) = args |> split_list ||> split_list;
     val name_atts = map (apsnd (map (prep_att thy))) raw_name_atts;
@@ -1008,7 +1007,7 @@
   let
     val _ = assert_backward state;
     val (goal_ctxt, (_, goal)) = find_goal state;
-    val {statement as (kind, propss, prop), messages, using, goal, before_qed, after_qed} = goal;
+    val {statement as (kind, _, prop), messages, using, goal, before_qed, after_qed} = goal;
     val goal_txt = prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt);
 
     val _ = is_relevant state andalso error "Cannot fork relevant proof";
--- a/src/Pure/Isar/proof_context.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Oct 01 15:19:49 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	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Isar/proof_node.ML	Thu Oct 01 15:19:49 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	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Thu Oct 01 15:19:49 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/Isar/specification.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Isar/specification.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -136,9 +136,6 @@
   prepare prep_vars parse_prop prep_att do_close
     vars (map single_spec specs) #>> apsnd (map the_spec);
 
-fun prep_specification prep_vars parse_prop prep_att vars specs =
-  prepare prep_vars parse_prop prep_att true [specs];
-
 in
 
 fun check_spec x = prep_spec ProofContext.cert_vars (K I) (K I) true x;
--- a/src/Pure/Isar/theory_target.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Isar/theory_target.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -45,7 +45,7 @@
 
 (* pretty *)
 
-fun pretty_thy ctxt target is_locale is_class =
+fun pretty_thy ctxt target is_class =
   let
     val thy = ProofContext.theory_of ctxt;
     val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
@@ -63,12 +63,12 @@
       (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)]
   end;
 
-fun pretty (Target {target, is_locale, is_class, instantiation, overloading, ...}) ctxt =
+fun pretty (Target {target, is_class, instantiation, overloading, ...}) ctxt =
   Pretty.block [Pretty.str "theory", Pretty.brk 1,
       Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] ::
     (if not (null overloading) then [Overloading.pretty ctxt]
      else if not (null (#1 instantiation)) then [Class_Target.pretty_instantiation ctxt]
-     else pretty_thy ctxt target is_locale is_class);
+     else pretty_thy ctxt target is_class);
 
 
 (* target declarations *)
@@ -260,8 +260,7 @@
 
 (* define *)
 
-fun define (ta as Target {target, is_locale, is_class, ...})
-    kind ((b, mx), ((name, atts), rhs)) lthy =
+fun define ta kind ((b, mx), ((name, atts), rhs)) lthy =
   let
     val thy = ProofContext.theory_of lthy;
     val thy_ctxt = ProofContext.init thy;
--- a/src/Pure/Isar/toplevel.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -126,7 +126,6 @@
   SkipProof of int * (generic_theory * generic_theory);
     (*proof depth, resulting theory, original theory*)
 
-val the_global_theory = fn Theory (Context.Theory thy, _) => thy | _ => raise UNDEF;
 val theory_node = fn Theory (gthy, _) => SOME gthy | _ => NONE;
 val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE;
 
@@ -256,7 +255,7 @@
 
 in
 
-fun apply_transaction pos f g (node, exit) =
+fun apply_transaction f g (node, exit) =
   let
     val _ = is_draft_theory node andalso error "Illegal draft theory in toplevel state";
     val cont_node = reset_presentation node;
@@ -293,29 +292,29 @@
 
 local
 
-fun apply_tr int _ (Init (_, f, exit)) (State (NONE, _)) =
+fun apply_tr int (Init (_, f, exit)) (State (NONE, _)) =
       State (SOME (Theory (Context.Theory (Theory.checkpoint (f int)), NONE), exit), NONE)
-  | apply_tr _ _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) =
+  | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) =
       State (NONE, prev)
-  | apply_tr _ _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =
+  | apply_tr _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =
       (Runtime.controlled_execution exit thy; toplevel)
-  | apply_tr int _ (Keep f) state =
+  | apply_tr int (Keep f) state =
       Runtime.controlled_execution (fn x => tap (f int) x) state
-  | apply_tr int pos (Transaction (f, g)) (State (SOME state, _)) =
-      apply_transaction pos (fn x => f int x) g state
-  | apply_tr _ _ _ _ = raise UNDEF;
+  | apply_tr int (Transaction (f, g)) (State (SOME state, _)) =
+      apply_transaction (fn x => f int x) g state
+  | apply_tr _ _ _ = raise UNDEF;
 
-fun apply_union _ _ [] state = raise FAILURE (state, UNDEF)
-  | apply_union int pos (tr :: trs) state =
-      apply_union int pos trs state
-        handle Runtime.UNDEF => apply_tr int pos tr state
-          | FAILURE (alt_state, UNDEF) => apply_tr int pos tr alt_state
+fun apply_union _ [] state = raise FAILURE (state, UNDEF)
+  | apply_union int (tr :: trs) state =
+      apply_union int trs state
+        handle Runtime.UNDEF => apply_tr int tr state
+          | FAILURE (alt_state, UNDEF) => apply_tr int tr alt_state
           | exn as FAILURE _ => raise exn
           | exn => raise FAILURE (state, exn);
 
 in
 
-fun apply_trans int pos trs state = (apply_union int pos trs state, NONE)
+fun apply_trans int trs state = (apply_union int trs state, NONE)
   handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn);
 
 end;
@@ -562,14 +561,14 @@
 
 local
 
-fun app int (tr as Transition {trans, pos, print, no_timing, ...}) =
+fun app int (tr as Transition {trans, print, no_timing, ...}) =
   setmp_thread_position tr (fn state =>
     let
       fun do_timing f x = (warning (command_msg "" tr); timeap f x);
       fun do_profiling f x = profile (! profiling) f x;
 
       val (result, status) =
-         state |> (apply_trans int pos trans
+         state |> (apply_trans int trans
           |> (if ! profiling > 0 andalso not no_timing then do_profiling else I)
           |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I));
 
--- a/src/Pure/Isar/value_parse.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Isar/value_parse.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -9,6 +9,7 @@
   val comma: 'a parser -> 'a parser
   val equal: 'a parser -> 'a parser
   val parens: 'a parser -> 'a parser
+  val unit: unit parser
   val pair: 'a parser -> 'b parser -> ('a * 'b) parser
   val triple: 'a parser -> 'b parser -> 'c parser -> ('a * 'b * 'c) parser
   val list: 'a parser -> 'a list parser
--- a/src/Pure/ML/ml_antiquote.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Thu Oct 01 15:19:49 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	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Proof/extraction.ML	Thu Oct 01 15:19:49 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	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Syntax/ast.ML	Thu Oct 01 15:19:49 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/mixfix.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -128,16 +128,6 @@
 
 fun const_mixfix c mx = (const_name mx c, fix_mixfix c mx);
 
-fun map_mixfix _ NoSyn = NoSyn
-  | map_mixfix f (Mixfix (sy, ps, p)) = Mixfix (f sy, ps, p)
-  | map_mixfix f (Delimfix sy) = Delimfix (f sy)
-  | map_mixfix f (InfixName (sy, p)) = InfixName (f sy, p)
-  | map_mixfix f (InfixlName (sy, p)) = InfixlName (f sy, p)
-  | map_mixfix f (InfixrName (sy, p)) = InfixrName (f sy, p)
-  | map_mixfix f (Binder (sy, p, q)) = Binder (f sy, p, q)
-  | map_mixfix _ Structure = Structure
-  | map_mixfix _ _ = raise Fail ("map_mixfix: illegal occurrence of unnamed infix");
-
 fun mixfix_args NoSyn = 0
   | mixfix_args (Mixfix (sy, _, _)) = SynExt.mfix_args sy
   | mixfix_args (Delimfix sy) = SynExt.mfix_args sy
--- a/src/Pure/Syntax/syn_ext.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -270,9 +270,9 @@
     fun rem_pri (Argument (s, _)) = Argument (s, chain_pri)
       | rem_pri sym = sym;
 
-    fun logify_types copy_prod (a as (Argument (s, p))) =
+    fun logify_types (a as (Argument (s, p))) =
           if s <> "prop" andalso is_logtype s then Argument (logic, p) else a
-      | logify_types _ a = a;
+      | logify_types a = a;
 
 
     val raw_symbs = read_mfix sy handle ERROR msg => err_in_mfix msg mfix;
@@ -305,7 +305,7 @@
       if convert andalso not copy_prod then
        (if lhs = "prop" then sprop else if is_logtype lhs then logic else lhs)
       else lhs;
-    val symbs' = map (logify_types copy_prod) symbs;
+    val symbs' = map logify_types symbs;
     val xprod = XProd (lhs', symbs', const', pri);
 
     val _ = (List.app check_pri pris; check_pri pri; check_blocks symbs');
--- a/src/Pure/Syntax/syn_trans.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -155,20 +155,11 @@
   | bigimpl_ast_tr (*"_bigimpl"*) asts = raise Ast.AST ("bigimpl_ast_tr", asts);
 
 
-(* meta conjunction *)
-
-fun conjunction_tr [t, u] = Lexicon.const "Pure.conjunction" $ t $ u
-  | conjunction_tr ts = raise TERM ("conjunction_tr", ts);
-
-
 (* type/term reflection *)
 
 fun type_tr (*"_TYPE"*) [ty] = mk_type ty
   | type_tr (*"_TYPE"*) ts = raise TERM ("type_tr", ts);
 
-fun term_tr [t] = Lexicon.const "Pure.term" $ t
-  | term_tr ts = raise TERM ("term_tr", ts);
-
 
 (* dddot *)
 
--- a/src/Pure/Syntax/syntax.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Syntax/syntax.ML	Thu Oct 01 15:19:49 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	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Thu Oct 01 15:19:49 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/System/isabelle_process.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/System/isabelle_process.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -133,6 +133,7 @@
  (Unsynchronized.change print_mode (update (op =) isabelle_processN);
   setup_channels out |> init_message;
   OuterKeyword.report ();
+  Isar_Document.init ();
   Output.status (Markup.markup Markup.ready "");
   Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
 
--- a/src/Pure/System/isar.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/System/isar.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -48,7 +48,6 @@
   in edit count (! global_state, ! global_history) end);
 
 fun state () = NAMED_CRITICAL "Isar" (fn () => ! global_state);
-fun set_state state = NAMED_CRITICAL "Isar" (fn () => global_state := state);
 
 fun exn () = NAMED_CRITICAL "Isar" (fn () => ! global_exn);
 fun set_exn exn =  NAMED_CRITICAL "Isar" (fn () => global_exn := exn);
--- a/src/Pure/Thy/html.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Thy/html.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -222,7 +222,6 @@
     in (implode syms, width) end;
 
 val output = #1 o output_width;
-val output_symbols = map #2 o output_syms;
 
 val _ = Output.add_mode htmlN output_width Symbol.encode_raw;
 
--- a/src/Pure/Thy/thy_info.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -283,7 +283,7 @@
 
 local
 
-fun provide path name info (deps as SOME {update_time, master, text, parents, files}) =
+fun provide path name info (SOME {update_time, master, text, parents, files}) =
      (if AList.defined (op =) files path then ()
       else warning (loader_msg "undeclared dependency of theory" [name] ^
         " on file: " ^ quote (Path.implode path));
@@ -338,7 +338,7 @@
 fun load_thy time upd_time initiators name =
   let
     val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
-    val (pos, text, files) =
+    val (pos, text, _) =
       (case get_deps name of
         SOME {master = SOME (master_path, _), text as _ :: _, files, ...} =>
           (Path.position master_path, text, files)
@@ -410,7 +410,7 @@
 
 in
 
-fun schedule_tasks tasks n =
+fun schedule_tasks tasks =
   if not (Multithreading.enabled ()) then schedule_seq tasks
   else if Multithreading.self_critical () then
      (warning (loader_msg "no multithreading within critical section" []);
@@ -438,7 +438,7 @@
   | NONE =>
       let val {master, text, imports = parents, uses = files} = ThyLoad.deps_thy dir name
       in (false, init_deps (SOME master) text parents files, parents) end
-  | SOME (deps as SOME {update_time, master, text, parents, files}) =>
+  | SOME (SOME {update_time, master, text, parents, files}) =>
       let
         val (thy_path, thy_id) = ThyLoad.check_thy dir name;
         val master' = SOME (thy_path, thy_id);
@@ -471,7 +471,7 @@
     val dir' = Path.append dir (Path.dir path);
     val _ = member (op =) initiators name andalso error (cycle_msg initiators);
   in
-    (case try (Graph.get_node (fst tasks)) name of
+    (case try (Graph.get_node tasks) name of
       SOME task => (task_finished task, tasks)
     | NONE =>
         let
@@ -481,7 +481,7 @@
                 required_by "\n" initiators);
           val parent_names = map base_name parents;
 
-          val (parents_current, (tasks_graph', tasks_len')) =
+          val (parents_current, tasks_graph') =
             require_thys time (name :: initiators)
               (Path.append dir (master_dir' deps)) parents tasks;
 
@@ -496,8 +496,7 @@
           val tasks_graph'' = tasks_graph' |> new_deps name parent_names
            (if all_current then Finished
             else Task (fn () => load_thy time upd_time initiators name));
-          val tasks_len'' = if all_current then tasks_len' else tasks_len' + 1;
-        in (all_current, (tasks_graph'', tasks_len'')) end)
+        in (all_current, tasks_graph'') end)
   end;
 
 end;
@@ -508,8 +507,7 @@
 local
 
 fun gen_use_thy' req dir arg =
-  let val (_, (tasks, n)) = req [] dir arg (Graph.empty, 0)
-  in schedule_tasks tasks n end;
+  schedule_tasks (snd (req [] dir arg Graph.empty));
 
 fun gen_use_thy req str =
   let val name = base_name str in
--- a/src/Pure/Tools/find_consts.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Tools/find_consts.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -107,7 +107,7 @@
                 val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
                 val sub_size =
                   Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0;
-              in SOME sub_size end handle MATCH => NONE
+              in SOME sub_size end handle Type.TYPE_MATCH => NONE
           end
       | make_match (Loose arg) =
           check_const (matches_subtype thy (make_pattern arg) o snd)
--- a/src/Pure/Tools/find_theorems.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -76,18 +76,9 @@
 
 fun is_nontrivial thy = Term.is_Const o Term.head_of o ObjectLogic.drop_judgment thy;
 
-(* Note: ("op =" : "bool --> bool --> bool") does not exist in Pure. *)
-fun is_Iff c =
-  (case dest_Const c of
-     ("op =", ty) =>
-       (ty
-        |> strip_type
-        |> swap
-        |> (op ::)
-        |> map (fst o dest_Type)
-        |> forall (curry (op =) "bool")
-        handle TYPE _ => false)
-   | _ => false);
+(*educated guesses on HOL*)  (* FIXME broken *)
+val boolT = Type ("bool", []);
+val iff_const = Const ("op =", boolT --> boolT --> boolT);
 
 (*extract terms from term_src, refine them to the parts that concern us,
   if po try match them against obj else vice versa.
@@ -97,19 +88,20 @@
   let
     val thy = ProofContext.theory_of ctxt;
 
-    val chkmatch = obj |> (if po then rpair else pair) #> Pattern.matches thy;
+    fun check_match pat = Pattern.matches thy (if po then (pat, obj) else (obj, pat));
     fun matches pat =
       let
         val jpat = ObjectLogic.drop_judgment thy pat;
         val c = Term.head_of jpat;
         val pats =
           if Term.is_Const c
-          then if doiff andalso is_Iff c
-               then pat :: map (ObjectLogic.ensure_propT thy) ((snd o strip_comb) jpat)
-                    |> filter (is_nontrivial thy)
-               else [pat]
+          then
+            if doiff andalso c = iff_const then
+              (pat :: map (ObjectLogic.ensure_propT thy) (snd (strip_comb jpat)))
+                |> filter (is_nontrivial thy)
+            else [pat]
           else [];
-      in filter chkmatch pats end;
+      in filter check_match pats end;
 
     fun substsize pat =
       let val (_, subst) =
@@ -117,12 +109,11 @@
       in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end;
 
     fun bestmatch [] = NONE
-     |  bestmatch xs = SOME (foldr1 Int.min xs);
+      | bestmatch xs = SOME (foldr1 Int.min xs);
 
     val match_thm = matches o refine_term;
   in
-    map match_thm (extract_terms term_src)
-    |> flat
+    maps match_thm (extract_terms term_src)
     |> map substsize
     |> bestmatch
   end;
@@ -178,8 +169,8 @@
         is_matching_thm false (single, I) ctxt true (goal_tree prem) rule_tree;
       val successful = prems |> map_filter try_subst;
     in
-    (*elim rules always have assumptions, so an elim with one
-      assumption is as good as an intro rule with none*)
+      (*elim rules always have assumptions, so an elim with one
+        assumption is as good as an intro rule with none*)
       if is_nontrivial (ProofContext.theory_of ctxt) (Thm.major_prem_of thm)
         andalso not (null successful)
       then SOME (Thm.nprems_of thm - 1, foldr1 Int.min successful) else NONE
@@ -190,15 +181,13 @@
 
 fun filter_solves ctxt goal =
   let
-    val baregoal = Logic.get_goal (Thm.prop_of goal) 1;
-
     fun etacn thm i = Seq.take (! tac_limit) o etac thm i;
     fun try_thm thm =
       if Thm.no_prems thm then rtac thm 1 goal
       else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
   in
     fn (_, thm) =>
-      if (is_some o Seq.pull o try_thm) thm
+      if is_some (Seq.pull (try_thm thm))
       then SOME (Thm.nprems_of thm, 0) else NONE
   end;
 
@@ -218,7 +207,7 @@
 
 (* filter_pattern *)
 
-fun get_names t = (Term.add_const_names t []) union (Term.add_free_names t []);
+fun get_names t = Term.add_const_names t (Term.add_free_names t []);
 fun get_thm_names (_, thm) = get_names (Thm.full_prop_of thm);
 
 (*Including all constants and frees is only sound because
@@ -238,10 +227,9 @@
 
     fun check (t, NONE) = check (t, SOME (get_thm_names t))
       | check ((_, thm), c as SOME thm_consts) =
-          (if pat_consts subset_string thm_consts
-              andalso (Pattern.matches_subterm (ProofContext.theory_of ctxt)
-                                               (pat, Thm.full_prop_of thm))
-           then SOME (0, 0) else NONE, c);
+         (if pat_consts subset_string thm_consts andalso
+            Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, Thm.full_prop_of thm)
+          then SOME (0, 0) else NONE, c);
   in check end;
 
 
@@ -253,7 +241,6 @@
   error ("Current goal required for " ^ c ^ " search criterion");
 
 val fix_goal = Thm.prop_of;
-val fix_goalo = Option.map fix_goal;
 
 fun filter_crit _ _ (Name name) = apfst (filter_name name)
   | filter_crit _ NONE Intro = err_no_goal "intro"
@@ -276,7 +263,7 @@
 fun app_filters thm =
   let
     fun app (NONE, _, _) = NONE
-      | app (SOME v, consts, []) = SOME (v, thm)
+      | app (SOME v, _, []) = SOME (v, thm)
       | app (r, consts, f :: fs) =
           let val (r', consts') = f (thm, consts)
           in app (opt_add r r', consts', fs) end;
@@ -439,6 +426,7 @@
   end;
 
 
+
 (** command syntax **)
 
 fun find_theorems_cmd ((opt_lim, rem_dups), spec) =
--- a/src/Pure/axclass.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/axclass.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -150,7 +150,6 @@
   let val params = #2 (get_axclasses thy);
   in fold (fn (x, c) => if pred c then cons x else I) params [] end;
 
-fun params_of thy c = get_params thy (fn c' => c' = c);
 fun all_params_of thy S = get_params thy (fn c => Sign.subsort thy (S, [c]));
 
 fun class_of_param thy = AList.lookup (op =) (#2 (get_axclasses thy));
@@ -263,7 +262,8 @@
 
 fun unoverload_const thy (c_ty as (c, _)) =
   case class_of_param thy c
-   of SOME class => (case get_inst_tyco (Sign.consts_of thy) c_ty
+   of SOME class (* FIXME unused? *) =>
+     (case get_inst_tyco (Sign.consts_of thy) c_ty
        of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
         | NONE => c)
     | NONE => c;
@@ -585,7 +585,7 @@
         val hyps = vars
           |> map (fn (T, S) => (T, Thm.of_sort (certT T, S) ~~ S));
         val ths = (typ, sort)
-          |> Sorts.of_sort_derivation (Syntax.pp_global thy) (Sign.classes_of thy)
+          |> Sorts.of_sort_derivation (Sign.classes_of thy)
            {class_relation =
               fn (th, c1) => fn c2 => th RS the_classrel thy (c1, c2),
             type_constructor =
--- a/src/Pure/consts.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/consts.ML	Thu Oct 01 15:19:49 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	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/context.ML	Thu Oct 01 15:19:49 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/defs.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/defs.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -123,7 +123,7 @@
 fun contained (U as TVar _) (Type (_, Ts)) = exists (fn T => T = U orelse contained U T) Ts
   | contained _ _ = false;
 
-fun acyclic pp defs (c, args) (d, Us) =
+fun acyclic pp (c, args) (d, Us) =
   c <> d orelse
   exists (fn U => exists (contained U) args) Us orelse
   is_none (match_args (args, Us)) orelse
@@ -150,7 +150,7 @@
       if forall (is_none o #1) reds then NONE
       else SOME (fold_rev
         (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
-    val _ = forall (acyclic pp defs const) (the_default deps deps');
+    val _ = forall (acyclic pp const) (the_default deps deps');
   in deps' end;
 
 in
@@ -163,8 +163,7 @@
           (args, perhaps (reduction pp defs (c, args)) deps));
       in
         if reducts = reducts' then (changed, defs)
-        else (true, defs |> map_def c (fn (specs, restricts, reducts) =>
-          (specs, restricts, reducts')))
+        else (true, defs |> map_def c (fn (specs, restricts, _) => (specs, restricts, reducts')))
       end;
     fun norm_all defs =
       (case Symtab.fold norm_update defs (false, defs) of
@@ -206,7 +205,7 @@
   let
     val restr =
       if plain_args args orelse
-        (case args of [Type (a, rec_args)] => plain_args rec_args | _ => false)
+        (case args of [Type (_, rec_args)] => plain_args rec_args | _ => false)
       then [] else [(args, name)];
     val spec =
       (serial (), {is_def = is_def, name = name, lhs = args, rhs = deps});
--- a/src/Pure/display.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/display.ML	Thu Oct 01 15:19:49 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/envir.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/envir.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -62,8 +62,8 @@
   tenv: tenv,           (*assignments to Vars*)
   tyenv: Type.tyenv};   (*assignments to TVars*)
 
-fun make_env (maxidx, tenv, tyenv) = Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv};
-fun map_env f (Envir {maxidx, tenv, tyenv}) = make_env (f (maxidx, tenv, tyenv));
+fun make_env (maxidx, tenv, tyenv) =
+  Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv};
 
 fun maxidx_of (Envir {maxidx, ...}) = maxidx;
 fun term_env (Envir {tenv, ...}) = tenv;
--- a/src/Pure/goal.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/goal.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -300,22 +300,22 @@
   | SOME st' => Seq.single st');
 
 (*parallel refinement of non-schematic goal by single results*)
+exception FAILED of unit;
 fun PARALLEL_GOALS tac st =
   let
     val st0 = Thm.adjust_maxidx_thm ~1 st;
     val _ = Thm.maxidx_of st0 >= 0 andalso
       raise THM ("PARALLEL_GOALS: schematic goal state", 0, [st]);
 
-    exception FAILED;
     fun try_tac g =
       (case SINGLE tac g of
-        NONE => raise FAILED
+        NONE => raise FAILED ()
       | SOME g' => g');
 
     val goals = Drule.strip_imp_prems (Thm.cprop_of st0);
     val results = Par_List.map (try_tac o init) goals;
   in ALLGOALS (fn i => retrofit i 1 (nth results (i - 1))) st0 end
-  handle FAILED => Seq.empty;
+  handle FAILED () => Seq.empty;
 
 end;
 
--- a/src/Pure/logic.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/logic.ML	Thu Oct 01 15:19:49 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/meta_simplifier.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/meta_simplifier.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -229,11 +229,6 @@
 
 fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2);
 
-fun map_simpset f (Simpset ({rules, prems, bounds, depth, context},
-    {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers})) =
-  make_simpset (f ((rules, prems, bounds, depth, context),
-    (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)));
-
 fun map_simpset1 f (Simpset (r1, r2)) = Simpset (map_ss1 f r1, r2);
 fun map_simpset2 f (Simpset (r1, r2)) = Simpset (r1, map_ss2 f r2);
 
@@ -388,7 +383,7 @@
     (Net.delete_term eq_rrule (term_of elhs, rrule) rules, prems, bounds, depth, context))
   handle Net.DELETE => (cond_warn_thm "Rewrite rule not in simpset:" ss thm; ss);
 
-fun insert_rrule (rrule as {thm, name, elhs, ...}) ss =
+fun insert_rrule (rrule as {thm, name, ...}) ss =
  (trace_named_thm (fn () => "Adding rewrite rule") ss (thm, name);
   ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) =>
     let
@@ -455,7 +450,6 @@
   | SOME eq_True =>
       let
         val (_, _, lhs, elhs, _, _) = decomp_simp eq_True;
-        val extra = rrule_extra_vars elhs eq_True;
       in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end);
 
 (*create the rewrite rule and possibly also the eq_True variant,
@@ -869,7 +863,7 @@
   Otherwise those vars may become instantiated with unnormalized terms
   while the premises are solved.*)
 
-fun cond_skel (args as (congs, (lhs, rhs))) =
+fun cond_skel (args as (_, (lhs, rhs))) =
   if Term.add_vars rhs [] subset Term.add_vars lhs [] then uncond_skel args
   else skel0;
 
@@ -892,8 +886,7 @@
     val eta_t = term_of eta_t';
     fun rew {thm, name, lhs, elhs, extra, fo, perm} =
       let
-        val thy = Thm.theory_of_thm thm;
-        val {prop, maxidx, ...} = rep_thm thm;
+        val prop = Thm.prop_of thm;
         val (rthm, elhs') =
           if maxt = ~1 orelse not extra then (thm, elhs)
           else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs);
@@ -979,7 +972,7 @@
       (* Thm.match can raise Pattern.MATCH;
          is handled when congc is called *)
       val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
-      val unit = trace_thm (fn () => "Applying congruence rule:") ss thm';
+      val _ = trace_thm (fn () => "Applying congruence rule:") ss thm';
       fun err (msg, thm) = (trace_thm (fn () => msg) ss thm; NONE)
   in case prover thm' of
        NONE => err ("Congruence proof failed.  Could not prove", thm')
@@ -1025,7 +1018,7 @@
 
     and subc skel (ss as Simpset ({bounds, ...}, {congs, ...})) t0 =
        (case term_of t0 of
-           Abs (a, T, t) =>
+           Abs (a, T, _) =>
              let
                  val b = Name.bound (#1 bounds);
                  val (v, t') = Thm.dest_abs (SOME b) t0;
@@ -1124,7 +1117,7 @@
       end
 
     and rebuild [] _ _ _ _ eq = eq
-      | rebuild (prem :: prems) concl (rrs :: rrss) (asm :: asms) ss eq =
+      | rebuild (prem :: prems) concl (_ :: rrss) (_ :: asms) ss eq =
           let
             val ss' = add_rrules (rev rrss, rev asms) ss;
             val concl' =
@@ -1231,7 +1224,7 @@
   let
     val thy = Thm.theory_of_cterm raw_ct;
     val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
-    val {t, maxidx, ...} = Thm.rep_cterm ct;
+    val {maxidx, ...} = Thm.rep_cterm ct;
     val ss = inc_simp_depth (activate_context thy raw_ss);
     val depth = simp_depth ss;
     val _ =
@@ -1297,8 +1290,8 @@
 (* for folding definitions, handling critical pairs *)
 
 (*The depth of nesting in a term*)
-fun term_depth (Abs(a,T,t)) = 1 + term_depth t
-  | term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t)
+fun term_depth (Abs (_, _, t)) = 1 + term_depth t
+  | term_depth (f $ t) = 1 + Int.max (term_depth f, term_depth t)
   | term_depth _ = 0;
 
 val lhs_of_thm = #1 o Logic.dest_equals o prop_of;
--- a/src/Pure/proofterm.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/proofterm.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -959,7 +959,7 @@
   if ! proofs = 0 then ((name, dummy), Oracle (name, dummy, NONE))
   else ((name, prop), gen_axm_proof Oracle name prop);
 
-fun shrink_proof thy =
+val shrink_proof =
   let
     fun shrink ls lev (prf as Abst (a, T, body)) =
           let val (b, is, ch, body') = shrink ls (lev+1) body
@@ -1319,7 +1319,7 @@
 
     val proof0 =
       if ! proofs = 2 then
-        #4 (shrink_proof thy [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)))
+        #4 (shrink_proof [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)))
       else MinProof;
     val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
 
--- a/src/Pure/pure_thy.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/pure_thy.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -239,7 +239,6 @@
 (*** Pure theory syntax and logical content ***)
 
 val typ = SimpleSyntax.read_typ;
-val term = SimpleSyntax.read_term;
 val prop = SimpleSyntax.read_prop;
 
 val typeT = Syntax.typeT;
--- a/src/Pure/sign.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/sign.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -68,7 +68,6 @@
   val certify_typ_mode: Type.mode -> theory -> typ -> typ
   val certify': bool -> Pretty.pp -> bool -> Consts.T -> theory -> term -> term * typ * int
   val certify_term: theory -> term -> term * typ * int
-  val certify_prop: theory -> term -> term * typ * int
   val cert_term: theory -> term -> term
   val cert_prop: theory -> term -> term
   val no_frees: Pretty.pp -> term -> term
@@ -369,11 +368,9 @@
   in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
 
 fun certify_term thy = certify' false (Syntax.pp_global thy) true (consts_of thy) thy;
-fun certify_prop thy = certify' true (Syntax.pp_global thy) true (consts_of thy) thy;
-
 fun cert_term_abbrev thy = #1 o certify' false (Syntax.pp_global thy) false (consts_of thy) thy;
 val cert_term = #1 oo certify_term;
-val cert_prop = #1 oo certify_prop;
+fun cert_prop thy = #1 o certify' true (Syntax.pp_global thy) true (consts_of thy) thy;
 
 end;
 
--- a/src/Pure/simplifier.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/simplifier.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -287,8 +287,6 @@
 
 val simpN = "simp";
 val congN = "cong";
-val addN = "add";
-val delN = "del";
 val onlyN = "only";
 val no_asmN = "no_asm";
 val no_asm_useN = "no_asm_use";
--- a/src/Pure/sorts.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/sorts.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -57,7 +57,7 @@
   val meet_sort_typ: algebra -> typ * sort -> typ -> typ   (*exception CLASS_ERROR*)
   val of_sort: algebra -> typ * sort -> bool
   val weaken: algebra -> ('a * class -> class -> 'a) -> 'a * class -> class -> 'a
-  val of_sort_derivation: Pretty.pp -> algebra ->
+  val of_sort_derivation: algebra ->
     {class_relation: 'a * class -> class -> 'a,
      type_constructor: string -> ('a * class) list list -> class -> 'a,
      type_variable: typ -> ('a * class) list} ->
@@ -401,7 +401,7 @@
     | cs :: _ => path (x, cs))
   end;
 
-fun of_sort_derivation pp algebra {class_relation, type_constructor, type_variable} =
+fun of_sort_derivation algebra {class_relation, type_constructor, type_variable} =
   let
     val weaken = weaken algebra class_relation;
     val arities = arities_of algebra;
--- a/src/Pure/term.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/term.ML	Thu Oct 01 15:19:49 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/theory.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/theory.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -94,7 +94,8 @@
   val empty = make_thy (NameSpace.empty_table, Defs.empty, ([], []));
   val copy = I;
 
-  fun extend (Thy {axioms, defs, wrappers}) = make_thy (NameSpace.empty_table, defs, wrappers);
+  fun extend (Thy {axioms = _, defs, wrappers}) =
+    make_thy (NameSpace.empty_table, defs, wrappers);
 
   fun merge pp (thy1, thy2) =
     let
@@ -155,7 +156,7 @@
 
 fun cert_axm thy (b, raw_tm) =
   let
-    val (t, T, _) = Sign.certify_prop thy raw_tm
+    val t = Sign.cert_prop thy raw_tm
       handle TYPE (msg, _, _) => error msg
         | TERM (msg, _) => error msg;
   in
--- a/src/Pure/thm.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/thm.ML	Thu Oct 01 15:19:49 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	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/type.ML	Thu Oct 01 15:19:49 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	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Pure/variable.ML	Thu Oct 01 15:19:49 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));
 );
--- a/src/Tools/Code/code_preproc.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -403,7 +403,7 @@
         @ (maps o maps) fst xs;
     fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
   in
-    flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
+    flat (Sorts.of_sort_derivation algebra
       { class_relation = class_relation, type_constructor = type_constructor,
         type_variable = type_variable } (T, proj_sort sort)
        handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
--- a/src/Tools/Code/code_thingol.ML	Thu Oct 01 15:19:23 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML	Thu Oct 01 15:19:49 2009 +0200
@@ -750,7 +750,6 @@
   #>> (fn sort => (unprefix "'" v, sort))
 and translate_dicts thy (algbr as (proj_sort, algebra)) funcgr thm (ty, sort) =
   let
-    val pp = Syntax.pp_global thy;
     datatype typarg =
         Global of (class * string) * typarg list list
       | Local of (class * class) list * (string * (int * sort));
@@ -764,7 +763,7 @@
       let
         val sort' = proj_sort sort;
       in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
-    val typargs = Sorts.of_sort_derivation pp algebra
+    val typargs = Sorts.of_sort_derivation algebra
       {class_relation = class_relation, type_constructor = type_constructor,
        type_variable = type_variable} (ty, proj_sort sort)
       handle Sorts.CLASS_ERROR e => not_wellsorted thy thm ty sort e;