merged
authorwenzelm
Thu Oct 01 11:33:32 2009 +0200 (2009-10-01)
changeset 32807c4f03b0cb753
parent 32806 06561afcadaa
parent 32799 7478ea535416
child 32808 0059238fe4bc
merged
src/Pure/Isar/expression.ML
     1.1 --- a/src/HOL/Record.thy	Thu Oct 01 09:09:56 2009 +0200
     1.2 +++ b/src/HOL/Record.thy	Thu Oct 01 11:33:32 2009 +0200
     1.3 @@ -450,10 +450,6 @@
     1.4    "Q = R \<Longrightarrow> (P \<and> Q) = (P \<and> R)"
     1.5    by simp
     1.6  
     1.7 -lemma meta_all_sameI:
     1.8 -  "(\<And>x. PROP P x \<equiv> PROP Q x) \<Longrightarrow> (\<And>x. PROP P x) \<equiv> (\<And>x. PROP Q x)"
     1.9 -  by simp
    1.10 -
    1.11  lemma istuple_UNIV_I: "\<And>x. x\<in>UNIV \<equiv> True"
    1.12    by simp
    1.13  
     2.1 --- a/src/HOL/Tools/record.ML	Thu Oct 01 09:09:56 2009 +0200
     2.2 +++ b/src/HOL/Tools/record.ML	Thu Oct 01 11:33:32 2009 +0200
     2.3 @@ -202,22 +202,18 @@
     2.4  struct
     2.5  
     2.6  val eq_reflection = @{thm eq_reflection};
     2.7 -val Pair_eq = @{thm Product_Type.prod.inject};
     2.8  val atomize_all = @{thm HOL.atomize_all};
     2.9  val atomize_imp = @{thm HOL.atomize_imp};
    2.10  val meta_allE = @{thm Pure.meta_allE};
    2.11  val prop_subst = @{thm prop_subst};
    2.12 -val Pair_sel_convs = [fst_conv, snd_conv];
    2.13  val K_record_comp = @{thm K_record_comp};
    2.14  val K_comp_convs = [@{thm o_apply}, K_record_comp]
    2.15 -val transitive_thm = @{thm transitive};
    2.16  val o_assoc = @{thm o_assoc};
    2.17  val id_apply = @{thm id_apply};
    2.18  val id_o_apps = [@{thm id_apply}, @{thm id_o}, @{thm o_id}];
    2.19  val Not_eq_iff = @{thm Not_eq_iff};
    2.20  
    2.21  val refl_conj_eq = @{thm refl_conj_eq};
    2.22 -val meta_all_sameI = @{thm meta_all_sameI};
    2.23  
    2.24  val surject_assistI = @{thm "istuple_surjective_proof_assistI"};
    2.25  val surject_assist_idE = @{thm "istuple_surjective_proof_assist_idE"};
    2.26 @@ -250,7 +246,6 @@
    2.27  val ext_typeN = "_ext_type";
    2.28  val inner_typeN = "_inner_type";
    2.29  val extN ="_ext";
    2.30 -val casesN = "_cases";
    2.31  val ext_dest = "_sel";
    2.32  val updateN = "_update";
    2.33  val updN = "_upd";
    2.34 @@ -259,10 +254,6 @@
    2.35  val extendN = "extend";
    2.36  val truncateN = "truncate";
    2.37  
    2.38 -(*see typedef.ML*)
    2.39 -val RepN = "Rep_";
    2.40 -val AbsN = "Abs_";
    2.41 -
    2.42  
    2.43  
    2.44  (*** utilities ***)
    2.45 @@ -273,24 +264,6 @@
    2.46    let fun varify (a, S) = TVar ((a, midx + 1), S);
    2.47    in map_type_tfree varify end;
    2.48  
    2.49 -fun domain_type' T =
    2.50 -  domain_type T handle Match => T;
    2.51 -
    2.52 -fun range_type' T =
    2.53 -  range_type T handle Match => T;
    2.54 -
    2.55 -
    2.56 -(* messages *)  (* FIXME proper context *)
    2.57 -
    2.58 -fun trace_thm str thm =
    2.59 -  tracing (str ^ Pretty.string_of (Display.pretty_thm_without_context thm));
    2.60 -
    2.61 -fun trace_thms str thms =
    2.62 -  (tracing str; map (trace_thm "") thms);
    2.63 -
    2.64 -fun trace_term str t =
    2.65 -  tracing (str ^ Syntax.string_of_term_global Pure.thy t);
    2.66 -
    2.67  
    2.68  (* timing *)
    2.69  
    2.70 @@ -302,7 +275,6 @@
    2.71  (* syntax *)
    2.72  
    2.73  fun prune n xs = Library.drop (n, xs);
    2.74 -fun prefix_base s = Long_Name.map_base_name (fn bname => s ^ bname);
    2.75  
    2.76  val Trueprop = HOLogic.mk_Trueprop;
    2.77  fun All xs t = Term.list_all_free (xs, t);
    2.78 @@ -311,22 +283,10 @@
    2.79  infix 0 :== ===;
    2.80  infixr 0 ==>;
    2.81  
    2.82 -val (op $$) = Term.list_comb;
    2.83 -val (op :==) = PrimitiveDefs.mk_defpair;
    2.84 -val (op ===) = Trueprop o HOLogic.mk_eq;
    2.85 -val (op ==>) = Logic.mk_implies;
    2.86 -
    2.87 -
    2.88 -(* morphisms *)
    2.89 -
    2.90 -fun mk_RepN name = suffix ext_typeN (prefix_base RepN name);
    2.91 -fun mk_AbsN name = suffix ext_typeN (prefix_base AbsN name);
    2.92 -
    2.93 -fun mk_Rep name repT absT =
    2.94 -  Const (suffix ext_typeN (prefix_base RepN name), absT --> repT);
    2.95 -
    2.96 -fun mk_Abs name repT absT =
    2.97 -  Const (mk_AbsN name, repT --> absT);
    2.98 +val op $$ = Term.list_comb;
    2.99 +val op :== = PrimitiveDefs.mk_defpair;
   2.100 +val op === = Trueprop o HOLogic.mk_eq;
   2.101 +val op ==> = Logic.mk_implies;
   2.102  
   2.103  
   2.104  (* constructor *)
   2.105 @@ -338,15 +298,6 @@
   2.106    in list_comb (Const (mk_extC (name, T) Ts), ts) end;
   2.107  
   2.108  
   2.109 -(* cases *)
   2.110 -
   2.111 -fun mk_casesC (name, T, vT) Ts = (suffix casesN name, (Ts ---> vT) --> T --> vT);
   2.112 -
   2.113 -fun mk_cases (name, T, vT) f =
   2.114 -  let val Ts = binder_types (fastype_of f)
   2.115 -  in Const (mk_casesC (name, T, vT) Ts) $ f end;
   2.116 -
   2.117 -
   2.118  (* selector *)
   2.119  
   2.120  fun mk_selC sT (c, T) = (c, sT --> T);
   2.121 @@ -369,7 +320,7 @@
   2.122  
   2.123  (* types *)
   2.124  
   2.125 -fun dest_recT (typ as Type (c_ext_type, Ts as (T :: _))) =
   2.126 +fun dest_recT (typ as Type (c_ext_type, Ts as (_ :: _))) =
   2.127        (case try (unsuffix ext_typeN) c_ext_type of
   2.128          NONE => raise TYPE ("Record.dest_recT", [typ], [])
   2.129        | SOME c => ((c, Ts), List.last Ts))
   2.130 @@ -549,8 +500,6 @@
   2.131  
   2.132  val get_simpset = get_ss_with_context #simpset;
   2.133  val get_sel_upd_defs = get_ss_with_context #defset;
   2.134 -val get_foldcong_ss = get_ss_with_context #foldcong;
   2.135 -val get_unfoldcong_ss = get_ss_with_context #unfoldcong;
   2.136  
   2.137  fun get_update_details u thy =
   2.138    let val sel_upd = get_sel_upd thy in
   2.139 @@ -618,8 +567,6 @@
   2.140        extfields fieldext;
   2.141    in RecordsData.put data thy end;
   2.142  
   2.143 -val get_extsplit = Symtab.lookup o #extsplit o RecordsData.get;
   2.144 -
   2.145  
   2.146  (* access 'splits' *)
   2.147  
   2.148 @@ -659,7 +606,7 @@
   2.149    let
   2.150      val ((name, Ts), moreT) = dest_recT T;
   2.151      val recname =
   2.152 -      let val (nm :: recn :: rst) = rev (Long_Name.explode name)
   2.153 +      let val (nm :: _ :: rst) = rev (Long_Name.explode name)   (* FIXME !? *)
   2.154        in Long_Name.implode (rev (nm :: rst)) end;
   2.155      val midx = maxidx_of_typs (moreT :: Ts);
   2.156      val varifyT = varifyT midx;
   2.157 @@ -698,7 +645,7 @@
   2.158  
   2.159  (* parent records *)
   2.160  
   2.161 -fun add_parents thy NONE parents = parents
   2.162 +fun add_parents _ NONE parents = parents
   2.163    | add_parents thy (SOME (types, name)) parents =
   2.164        let
   2.165          fun err msg = error (msg ^ " parent record " ^ quote name);
   2.166 @@ -787,7 +734,7 @@
   2.167        | splitargs (_ :: _) [] = raise TERM (msg ^ "expecting more fields", [t])
   2.168        | splitargs _ _ = ([], []);
   2.169  
   2.170 -    fun mk_ext (fargs as (name, arg) :: _) =
   2.171 +    fun mk_ext (fargs as (name, _) :: _) =
   2.172            (case get_fieldext thy (Sign.intern_const thy name) of
   2.173              SOME (ext, _) =>
   2.174                (case get_extfields thy ext of
   2.175 @@ -816,7 +763,7 @@
   2.176        | splitargs (_ :: _) [] = raise TERM (msg ^ "expecting more fields", [t])
   2.177        | splitargs _ _ = ([], []);
   2.178  
   2.179 -    fun mk_ext (fargs as (name, arg) :: _) =
   2.180 +    fun mk_ext (fargs as (name, _) :: _) =
   2.181            (case get_fieldext thy (Sign.intern_const thy name) of
   2.182              SOME (ext, alphas) =>
   2.183                (case get_extfields thy ext of
   2.184 @@ -838,7 +785,7 @@
   2.185                      val more' = mk_ext rest;
   2.186                    in
   2.187                      list_comb (Syntax.const (suffix sfx ext), alphas' @ [more'])
   2.188 -                  end handle TYPE_MATCH =>
   2.189 +                  end handle Type.TYPE_MATCH =>
   2.190                      raise TERM (msg ^ "type is no proper record (extension)", [t]))
   2.191                | NONE => raise TERM (msg ^ "no fields defined for " ^ ext, [t]))
   2.192            | NONE => raise TERM (msg ^ name ^" is no proper field", [t]))
   2.193 @@ -896,7 +843,7 @@
   2.194            (case k of
   2.195              Abs (_, _, Abs (_, _, t) $ Bound 0) =>
   2.196                if null (loose_bnos t) then t else raise Match
   2.197 -          | Abs (x, _, t) =>
   2.198 +          | Abs (_, _, t) =>
   2.199                if null (loose_bnos t) then t else raise Match
   2.200            | _ => raise Match);
   2.201  
   2.202 @@ -1012,7 +959,7 @@
   2.203                if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree (zeta, Sign.defaultS thy))))
   2.204                then mk_type_abbr subst abbr alphas
   2.205                else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
   2.206 -            end handle TYPE_MATCH => default_tr' ctxt tm)
   2.207 +            end handle Type.TYPE_MATCH => default_tr' ctxt tm)
   2.208            else raise Match (*give print translation of specialised record a chance*)
   2.209        | _ => raise Match)
   2.210      else default_tr' ctxt tm
   2.211 @@ -1045,8 +992,7 @@
   2.212                          val subst = fold2 (curry (Sign.typ_match thy)) alphavars args' Vartab.empty;
   2.213                          val flds'' = (map o apsnd) (Envir.norm_type subst o varifyT) flds';
   2.214                        in flds'' @ field_lst more end
   2.215 -                      handle TYPE_MATCH => [("", T)]
   2.216 -                        | Library.UnequalLengths => [("", T)])
   2.217 +                      handle Type.TYPE_MATCH => [("", T)] | Library.UnequalLengths => [("", T)])
   2.218                    | NONE => [("", T)])
   2.219                | NONE => [("", T)])
   2.220            | NONE => [("", T)])
   2.221 @@ -1106,7 +1052,8 @@
   2.222    then noopt ()
   2.223    else opt ();
   2.224  
   2.225 -fun is_sel_upd_pair thy (Const (s, t)) (Const (u, t')) =
   2.226 +(* FIXME non-standard name for partial identity; rename to check_... (??) *)
   2.227 +fun is_sel_upd_pair thy (Const (s, _)) (Const (u, t')) =
   2.228    (case get_updates thy u of
   2.229      SOME u_name => u_name = s
   2.230    | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]));
   2.231 @@ -1130,7 +1077,6 @@
   2.232  fun get_accupd_simps thy term defset intros_tac =
   2.233    let
   2.234      val (acc, [body]) = strip_comb term;
   2.235 -    val recT = domain_type (fastype_of acc);
   2.236      val upd_funs = sort_distinct TermOrd.fast_term_ord (get_upd_funs body);
   2.237      fun get_simp upd =
   2.238        let
   2.239 @@ -1140,10 +1086,10 @@
   2.240            if is_sel_upd_pair thy acc upd
   2.241            then mk_comp (Free ("f", T)) acc
   2.242            else mk_comp_id acc;
   2.243 -        val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   2.244 +        val prop = lhs === rhs;
   2.245          val othm =
   2.246            Goal.prove (ProofContext.init thy) [] [] prop
   2.247 -            (fn prems =>
   2.248 +            (fn _ =>
   2.249                EVERY
   2.250                 [simp_tac defset 1,
   2.251                  REPEAT_DETERM (intros_tac 1),
   2.252 @@ -1164,10 +1110,10 @@
   2.253        if comp
   2.254        then u $ mk_comp f f'
   2.255        else mk_comp (u' $ f') (u $ f);
   2.256 -    val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   2.257 +    val prop = lhs === rhs;
   2.258      val othm =
   2.259        Goal.prove (ProofContext.init thy) [] [] prop
   2.260 -        (fn prems =>
   2.261 +        (fn _ =>
   2.262            EVERY
   2.263             [simp_tac defset 1,
   2.264              REPEAT_DETERM (intros_tac 1),
   2.265 @@ -1177,11 +1123,10 @@
   2.266  
   2.267  fun get_updupd_simps thy term defset intros_tac =
   2.268    let
   2.269 -    val recT = fastype_of term;
   2.270      val upd_funs = get_upd_funs term;
   2.271      val cname = fst o dest_Const;
   2.272      fun getswap u u' = get_updupd_simp thy defset intros_tac u u' (cname u = cname u');
   2.273 -    fun build_swaps_to_eq upd [] swaps = swaps
   2.274 +    fun build_swaps_to_eq _ [] swaps = swaps
   2.275        | build_swaps_to_eq upd (u :: us) swaps =
   2.276            let
   2.277              val key = (cname u, cname upd);
   2.278 @@ -1192,7 +1137,7 @@
   2.279              if cname u = cname upd then newswaps
   2.280              else build_swaps_to_eq upd us newswaps
   2.281            end;
   2.282 -    fun swaps_needed [] prev seen swaps = map snd (Symreltab.dest swaps)
   2.283 +    fun swaps_needed [] _ _ swaps = map snd (Symreltab.dest swaps)
   2.284        | swaps_needed (u :: us) prev seen swaps =
   2.285            if Symtab.defined seen (cname u)
   2.286            then swaps_needed us prev seen (build_swaps_to_eq u prev swaps)
   2.287 @@ -1201,20 +1146,20 @@
   2.288  
   2.289  val named_cterm_instantiate = IsTupleSupport.named_cterm_instantiate;
   2.290  
   2.291 -fun prove_unfold_defs thy ss T ex_simps ex_simprs prop =
   2.292 +fun prove_unfold_defs thy ex_simps ex_simprs prop =
   2.293    let
   2.294      val defset = get_sel_upd_defs thy;
   2.295      val in_tac = IsTupleSupport.istuple_intros_tac thy;
   2.296      val prop' = Envir.beta_eta_contract prop;
   2.297 -    val (lhs, rhs) = Logic.dest_equals (Logic.strip_assums_concl prop');
   2.298 -    val (head, args) = strip_comb lhs;
   2.299 +    val (lhs, _) = Logic.dest_equals (Logic.strip_assums_concl prop');
   2.300 +    val (_, args) = strip_comb lhs;
   2.301      val simps =
   2.302        if length args = 1
   2.303        then get_accupd_simps thy lhs defset in_tac
   2.304        else get_updupd_simps thy lhs defset in_tac;
   2.305    in
   2.306      Goal.prove (ProofContext.init thy) [] [] prop'
   2.307 -      (fn prems =>
   2.308 +      (fn _ =>
   2.309          simp_tac (HOL_basic_ss addsimps (simps @ [K_record_comp])) 1 THEN
   2.310          TRY (simp_tac (HOL_basic_ss addsimps ex_simps addsimprocs ex_simprs) 1))
   2.311    end;
   2.312 @@ -1251,55 +1196,52 @@
   2.313  *)
   2.314  val record_simproc =
   2.315    Simplifier.simproc @{theory HOL} "record_simp" ["x"]
   2.316 -    (fn thy => fn ss => fn t =>
   2.317 +    (fn thy => fn _ => fn t =>
   2.318        (case t of
   2.319 -        (sel as Const (s, Type (_, [domS, rangeS]))) $
   2.320 +        (sel as Const (s, Type (_, [_, rangeS]))) $
   2.321              ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) =>
   2.322 -          if is_selector thy s then
   2.323 -            (case get_updates thy u of
   2.324 -              SOME u_name =>
   2.325 -                let
   2.326 -                  val {sel_upd = {updates, ...}, extfields, ...} = RecordsData.get thy;
   2.327 -
   2.328 -                  fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) =
   2.329 -                        (case Symtab.lookup updates u of
   2.330 -                          NONE => NONE
   2.331 -                        | SOME u_name =>
   2.332 -                            if u_name = s then
   2.333 -                              (case mk_eq_terms r of
   2.334 -                                NONE =>
   2.335 -                                  let
   2.336 -                                    val rv = ("r", rT);
   2.337 -                                    val rb = Bound 0;
   2.338 -                                    val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
   2.339 -                                  in SOME (upd $ kb $ rb, kb $ (sel $ rb), [kv, rv]) end
   2.340 -                              | SOME (trm, trm', vars) =>
   2.341 -                                  let
   2.342 -                                    val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k;
   2.343 -                                  in SOME (upd $ kb $ trm, kb $ trm', kv :: vars) end)
   2.344 -                            else if has_field extfields u_name rangeS orelse
   2.345 -                              has_field extfields s (domain_type kT) then NONE
   2.346 -                            else
   2.347 -                              (case mk_eq_terms r of
   2.348 -                                SOME (trm, trm', vars) =>
   2.349 -                                  let val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k
   2.350 -                                  in SOME (upd $ kb $ trm, trm', kv :: vars) end
   2.351 -                              | NONE =>
   2.352 -                                  let
   2.353 -                                    val rv = ("r", rT);
   2.354 -                                    val rb = Bound 0;
   2.355 -                                    val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
   2.356 -                                  in SOME (upd $ kb $ rb, sel $ rb, [kv, rv]) end))
   2.357 -                    | mk_eq_terms r = NONE;
   2.358 -                in
   2.359 -                  (case mk_eq_terms (upd $ k $ r) of
   2.360 -                    SOME (trm, trm', vars) =>
   2.361 -                      SOME
   2.362 -                        (prove_unfold_defs thy ss domS [] []
   2.363 -                          (list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
   2.364 -                  | NONE => NONE)
   2.365 -                end
   2.366 -            | NONE => NONE)
   2.367 +          if is_selector thy s andalso is_some (get_updates thy u) then
   2.368 +            let
   2.369 +              val {sel_upd = {updates, ...}, extfields, ...} = RecordsData.get thy;
   2.370 +
   2.371 +              fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) =
   2.372 +                    (case Symtab.lookup updates u of
   2.373 +                      NONE => NONE
   2.374 +                    | SOME u_name =>
   2.375 +                        if u_name = s then
   2.376 +                          (case mk_eq_terms r of
   2.377 +                            NONE =>
   2.378 +                              let
   2.379 +                                val rv = ("r", rT);
   2.380 +                                val rb = Bound 0;
   2.381 +                                val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
   2.382 +                              in SOME (upd $ kb $ rb, kb $ (sel $ rb), [kv, rv]) end
   2.383 +                          | SOME (trm, trm', vars) =>
   2.384 +                              let
   2.385 +                                val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k;
   2.386 +                              in SOME (upd $ kb $ trm, kb $ trm', kv :: vars) end)
   2.387 +                        else if has_field extfields u_name rangeS orelse
   2.388 +                          has_field extfields s (domain_type kT) then NONE
   2.389 +                        else
   2.390 +                          (case mk_eq_terms r of
   2.391 +                            SOME (trm, trm', vars) =>
   2.392 +                              let val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k
   2.393 +                              in SOME (upd $ kb $ trm, trm', kv :: vars) end
   2.394 +                          | NONE =>
   2.395 +                              let
   2.396 +                                val rv = ("r", rT);
   2.397 +                                val rb = Bound 0;
   2.398 +                                val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
   2.399 +                              in SOME (upd $ kb $ rb, sel $ rb, [kv, rv]) end))
   2.400 +                | mk_eq_terms _ = NONE;
   2.401 +            in
   2.402 +              (case mk_eq_terms (upd $ k $ r) of
   2.403 +                SOME (trm, trm', vars) =>
   2.404 +                  SOME
   2.405 +                    (prove_unfold_defs thy [] []
   2.406 +                      (list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
   2.407 +              | NONE => NONE)
   2.408 +            end
   2.409            else NONE
   2.410        | _ => NONE));
   2.411  
   2.412 @@ -1311,7 +1253,7 @@
   2.413      val prop = concl_of (named_cterm_instantiate insts updacc_cong_triv);
   2.414    in
   2.415      Goal.prove (ProofContext.init thy) [] [] prop
   2.416 -      (fn prems =>
   2.417 +      (fn _ =>
   2.418          EVERY
   2.419           [simp_tac simpset 1,
   2.420            REPEAT_DETERM (in_tac 1),
   2.421 @@ -1331,7 +1273,7 @@
   2.422    both a more update and an update to a field within it.*)
   2.423  val record_upd_simproc =
   2.424    Simplifier.simproc @{theory HOL} "record_upd_simp" ["x"]
   2.425 -    (fn thy => fn ss => fn t =>
   2.426 +    (fn thy => fn _ => fn t =>
   2.427        let
   2.428          (*We can use more-updators with other updators as long
   2.429            as none of the other updators go deeper than any more
   2.430 @@ -1346,7 +1288,7 @@
   2.431                then SOME (if min <= dep then dep else min, max)
   2.432                else NONE;
   2.433  
   2.434 -        fun getupdseq (term as (upd as Const (u, T)) $ f $ tm) min max =
   2.435 +        fun getupdseq (term as (upd as Const (u, _)) $ f $ tm) min max =
   2.436                (case get_update_details u thy of
   2.437                  SOME (s, dep, ismore) =>
   2.438                    (case include_depth (dep, ismore) (min, max) of
   2.439 @@ -1359,15 +1301,14 @@
   2.440  
   2.441          val (upds, base, baseT) = getupdseq t 0 ~1;
   2.442  
   2.443 -        fun is_upd_noop s (f as Abs (n, T, Const (s', T') $ tm')) tm =
   2.444 +        fun is_upd_noop s (Abs (n, T, Const (s', T') $ tm')) tm =
   2.445                if s = s' andalso null (loose_bnos tm')
   2.446                  andalso subst_bound (HOLogic.unit, tm') = tm
   2.447                then (true, Abs (n, T, Const (s', T') $ Bound 1))
   2.448                else (false, HOLogic.unit)
   2.449 -          | is_upd_noop s f tm = (false, HOLogic.unit);
   2.450 -
   2.451 -        fun get_noop_simps (upd as Const (u, T))
   2.452 -            (f as Abs (n, T', (acc as Const (s, T'')) $ _)) =
   2.453 +          | is_upd_noop _ _ _ = (false, HOLogic.unit);
   2.454 +
   2.455 +        fun get_noop_simps (upd as Const _) (Abs (_, _, (acc as Const _) $ _)) =
   2.456            let
   2.457              val ss = get_sel_upd_defs thy;
   2.458              val uathm = get_upd_acc_cong_thm upd acc thy ss;
   2.459 @@ -1417,17 +1358,16 @@
   2.460                        fvar :: vars, dups, true, noops)
   2.461                    | NONE => (upd $ skelf $ lhs, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops))
   2.462                end
   2.463 -          | mk_updterm [] above term =
   2.464 +          | mk_updterm [] _ _ =
   2.465                (Bound 0, Bound 0, [("r", baseT)], Symtab.empty, false, Symtab.empty)
   2.466 -          | mk_updterm us above term =
   2.467 -              raise TERM ("mk_updterm match", map (fn (x, y, z) => x) us);
   2.468 -
   2.469 -        val (lhs, rhs, vars, dups, simp, noops) = mk_updterm upds Symtab.empty base;
   2.470 +          | mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _) => x) us);
   2.471 +
   2.472 +        val (lhs, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base;
   2.473          val noops' = flat (map snd (Symtab.dest noops));
   2.474        in
   2.475          if simp then
   2.476            SOME
   2.477 -            (prove_unfold_defs thy ss baseT noops' [record_simproc]
   2.478 +            (prove_unfold_defs thy noops' [record_simproc]
   2.479                (list_all (vars, Logic.mk_equals (lhs, rhs))))
   2.480          else NONE
   2.481        end);
   2.482 @@ -1473,11 +1413,11 @@
   2.483    Simplifier.simproc @{theory HOL} "record_split_simp" ["x"]
   2.484      (fn thy => fn _ => fn t =>
   2.485        (case t of
   2.486 -        Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ trm =>
   2.487 +        Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
   2.488            if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex" then
   2.489              (case rec_id ~1 T of
   2.490                "" => NONE
   2.491 -            | name =>
   2.492 +            | _ =>
   2.493                  let val split = P t in
   2.494                    if split <> 0 then
   2.495                      (case get_splits thy (rec_id split T) of
   2.496 @@ -1568,10 +1508,10 @@
   2.497            simp_tac (HOL_basic_ss addsimps @{thms induct_rulify}) i]
   2.498        end;
   2.499  
   2.500 -    fun split_free_tac P i (free as Free (n, T)) =
   2.501 +    fun split_free_tac P i (free as Free (_, T)) =
   2.502            (case rec_id ~1 T of
   2.503              "" => NONE
   2.504 -          | name =>
   2.505 +          | _ =>
   2.506                let val split = P free in
   2.507                  if split <> 0 then
   2.508                    (case get_splits thy (rec_id split T) of
   2.509 @@ -1598,8 +1538,6 @@
   2.510  (*Split all records in the goal, which are quantified by ! or !!.*)
   2.511  fun record_split_tac i st =
   2.512    let
   2.513 -    val thy = Thm.theory_of_thm st;
   2.514 -
   2.515      val has_rec = exists_Const
   2.516        (fn (s, Type (_, [Type (_, [T, _]), _])) =>
   2.517            (s = "all" orelse s = "All") andalso is_recT T
   2.518 @@ -1695,40 +1633,16 @@
   2.519    in compose_tac (false, rule'', nprems_of rule) i st end;
   2.520  
   2.521  
   2.522 -(*!!x1 ... xn. ... ==> EX x1 ... xn. P x1 ... xn;
   2.523 -  instantiates x1 ... xn with parameters x1 ... xn*)
   2.524 -fun ex_inst_tac i st =
   2.525 -  let
   2.526 -    val thy = Thm.theory_of_thm st;
   2.527 -    val g = nth (prems_of st) (i - 1);   (* FIXME SUBGOAL *)
   2.528 -    val params = Logic.strip_params g;
   2.529 -    val exI' = Thm.lift_rule (Thm.cprem_of st i) exI;
   2.530 -    val _ $ (_ $ x) = Logic.strip_assums_concl (hd (prems_of exI'));
   2.531 -    val cx = cterm_of thy (fst (strip_comb x));
   2.532 -  in
   2.533 -    Seq.single (Library.foldl (fn (st, v) =>
   2.534 -      Seq.hd
   2.535 -        (compose_tac
   2.536 -          (false,
   2.537 -            cterm_instantiate [(cx, cterm_of thy (list_abs (params, Bound v)))] exI', 1) i st))
   2.538 -        (st, (length params - 1) downto 0))
   2.539 -  end;
   2.540 -
   2.541 -fun extension_definition full name fields names alphas zeta moreT more vars thy =
   2.542 +fun extension_definition name fields alphas zeta moreT more vars thy =
   2.543    let
   2.544      val base = Long_Name.base_name;
   2.545      val fieldTs = (map snd fields);
   2.546      val alphas_zeta = alphas @ [zeta];
   2.547      val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) alphas_zeta;
   2.548 -    val vT = TFree (Name.variant alphas_zeta "'v", HOLogic.typeS);
   2.549      val extT_name = suffix ext_typeN name
   2.550      val extT = Type (extT_name, alphas_zetaTs);
   2.551 -    val fields_more = fields @ [(full moreN, moreT)];
   2.552      val fields_moreTs = fieldTs @ [moreT];
   2.553 -    val bfields_more = map (apfst base) fields_more;
   2.554 -    val r = Free (rN, extT);
   2.555 -    val len = length fields;
   2.556 -    val idxms = 0 upto len;
   2.557 +
   2.558  
   2.559      (*before doing anything else, create the tree of new types
   2.560        that will back the record extension*)
   2.561 @@ -1739,7 +1653,7 @@
   2.562        let
   2.563          val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
   2.564          val nm = suffix suff (Long_Name.base_name name);
   2.565 -        val (isom, cons, thy') =
   2.566 +        val (_, cons, thy') =
   2.567            IsTupleSupport.add_istuple_type
   2.568              (nm, alphas_zeta) (fastype_of left, fastype_of right) thy;
   2.569        in
   2.570 @@ -1763,7 +1677,7 @@
   2.571              build_meta_tree_type i' thy' composites more
   2.572            end
   2.573          else
   2.574 -          let val (term, (thy', i')) = mk_istuple (mktreeV vars, more) (thy, 0)
   2.575 +          let val (term, (thy', _)) = mk_istuple (mktreeV vars, more) (thy, 0)
   2.576            in (term, thy') end
   2.577        end;
   2.578  
   2.579 @@ -1795,16 +1709,15 @@
   2.580      val ([ext_def], defs_thy) =
   2.581        timeit_msg "record extension constructor def:" mk_defs;
   2.582  
   2.583 +
   2.584      (* prepare propositions *)
   2.585 +
   2.586      val _ = timing_msg "record extension preparing propositions";
   2.587      val vars_more = vars @ [more];
   2.588 -    val named_vars_more = (names @ [full moreN]) ~~ vars_more;
   2.589      val variants = map (fn Free (x, _) => x) vars_more;
   2.590      val ext = mk_ext vars_more;
   2.591      val s = Free (rN, extT);
   2.592 -    val w = Free (wN, extT);
   2.593      val P = Free (Name.variant variants "P", extT --> HOLogic.boolT);
   2.594 -    val C = Free (Name.variant variants "C", HOLogic.boolT);
   2.595      val intros_tac = IsTupleSupport.istuple_intros_tac defs_thy;
   2.596  
   2.597      val inject_prop =
   2.598 @@ -1819,27 +1732,18 @@
   2.599      val induct_prop =
   2.600        (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
   2.601  
   2.602 -    val cases_prop =
   2.603 -      All (map dest_Free vars_more)
   2.604 -        (Trueprop (HOLogic.mk_eq (s, ext)) ==> Trueprop C)
   2.605 -      ==> Trueprop C;
   2.606 -
   2.607      val split_meta_prop =
   2.608 -      let val P = Free (Name.variant variants "P", extT-->Term.propT) in
   2.609 +      let val P = Free (Name.variant variants "P", extT --> Term.propT) in
   2.610          Logic.mk_equals
   2.611           (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
   2.612        end;
   2.613  
   2.614 -    fun prove stndrd = quick_and_dirty_prove stndrd defs_thy;
   2.615      val prove_standard = quick_and_dirty_prove true defs_thy;
   2.616 -    fun prove_simp stndrd simps =
   2.617 -      let val tac = simp_all_tac HOL_ss simps
   2.618 -      in fn prop => prove stndrd [] prop (K tac) end;
   2.619  
   2.620      fun inject_prf () =
   2.621        simplify HOL_ss
   2.622          (prove_standard [] inject_prop
   2.623 -          (fn prems =>
   2.624 +          (fn _ =>
   2.625              EVERY
   2.626               [simp_tac (HOL_basic_ss addsimps [ext_def]) 1,
   2.627                REPEAT_DETERM (resolve_tac [refl_conj_eq] 1 ORELSE
   2.628 @@ -1872,7 +1776,7 @@
   2.629  
   2.630      fun split_meta_prf () =
   2.631        prove_standard [] split_meta_prop
   2.632 -        (fn prems =>
   2.633 +        (fn _ =>
   2.634            EVERY
   2.635             [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
   2.636              etac meta_allE 1, atac 1,
   2.637 @@ -1909,8 +1813,8 @@
   2.638    | chop_last [x] = ([], x)
   2.639    | chop_last (x :: xs) = let val (tl, l) = chop_last xs in (x :: tl, l) end;
   2.640  
   2.641 -fun subst_last s [] = error "subst_last: list should not be empty"
   2.642 -  | subst_last s [x] = [s]
   2.643 +fun subst_last _ [] = error "subst_last: list should not be empty"
   2.644 +  | subst_last s [_] = [s]
   2.645    | subst_last s (x :: xs) = x :: subst_last s xs;
   2.646  
   2.647  
   2.648 @@ -1965,7 +1869,6 @@
   2.649      val parent_variants = Name.variant_list [moreN, rN, rN ^ "'", wN] (map base parent_names);
   2.650      val parent_vars = ListPair.map Free (parent_variants, parent_types);
   2.651      val parent_len = length parents;
   2.652 -    val parents_idx = (map #name parents) ~~ (0 upto (parent_len - 1));
   2.653  
   2.654      val fields = map (apfst full) bfields;
   2.655      val names = map fst fields;
   2.656 @@ -1979,13 +1882,10 @@
   2.657          (map fst bfields);
   2.658      val vars = ListPair.map Free (variants, types);
   2.659      val named_vars = names ~~ vars;
   2.660 -    val idxs = 0 upto (len - 1);
   2.661      val idxms = 0 upto len;
   2.662  
   2.663      val all_fields = parent_fields @ fields;
   2.664 -    val all_names = parent_names @ names;
   2.665      val all_types = parent_types @ types;
   2.666 -    val all_len = parent_fields_len + len;
   2.667      val all_variants = parent_variants @ variants;
   2.668      val all_vars = parent_vars @ vars;
   2.669      val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
   2.670 @@ -1997,7 +1897,6 @@
   2.671      val full_moreN = full moreN;
   2.672      val bfields_more = bfields @ [(moreN, moreT)];
   2.673      val fields_more = fields @ [(full_moreN, moreT)];
   2.674 -    val vars_more = vars @ [more];
   2.675      val named_vars_more = named_vars @ [(full_moreN, more)];
   2.676      val all_vars_more = all_vars @ [more];
   2.677      val all_named_vars_more = all_named_vars @ [(full_moreN, more)];
   2.678 @@ -2008,7 +1907,7 @@
   2.679      val (extension_thy, extT, ext_induct, ext_inject, ext_split, ext_def) =
   2.680        thy
   2.681        |> Sign.add_path bname
   2.682 -      |> extension_definition full extN fields names alphas_ext zeta moreT more vars;
   2.683 +      |> extension_definition extN fields alphas_ext zeta moreT more vars;
   2.684  
   2.685      val _ = timing_msg "record preparing definitions";
   2.686      val Type extension_scheme = extT;
   2.687 @@ -2080,16 +1979,6 @@
   2.688  
   2.689      (* prepare definitions *)
   2.690  
   2.691 -    fun parent_more s =
   2.692 -      if null parents then s
   2.693 -      else mk_sel s (Long_Name.qualify (#name (List.last parents)) moreN, extT);
   2.694 -
   2.695 -    fun parent_more_upd v s =
   2.696 -      if null parents then v $ s
   2.697 -      else
   2.698 -        let val mp = Long_Name.qualify (#name (List.last parents)) moreN;
   2.699 -        in mk_upd updateN mp v s end;
   2.700 -
   2.701      (*record (scheme) type abbreviation*)
   2.702      val recordT_specs =
   2.703        [(Binding.name (suffix schemeN bname), alphas @ [zeta], rec_schemeT0, Syntax.NoSyn),
   2.704 @@ -2233,14 +2122,12 @@
   2.705  
   2.706      (*cases*)
   2.707      val cases_scheme_prop =
   2.708 -      (All (map dest_Free all_vars_more)
   2.709 -        (Trueprop (HOLogic.mk_eq (r0, r_rec0)) ==> Trueprop C))
   2.710 -      ==> Trueprop C;
   2.711 +      (All (map dest_Free all_vars_more) (r0 === r_rec0 ==> Trueprop C))
   2.712 +        ==> Trueprop C;
   2.713  
   2.714      val cases_prop =
   2.715 -      (All (map dest_Free all_vars)
   2.716 -        (Trueprop (HOLogic.mk_eq (r_unit0, r_rec_unit0)) ==> Trueprop C))
   2.717 -       ==> Trueprop C;
   2.718 +      (All (map dest_Free all_vars) (r_unit0 === r_rec_unit0 ==> Trueprop C))
   2.719 +         ==> Trueprop C;
   2.720  
   2.721      (*split*)
   2.722      val split_meta_prop =
   2.723 @@ -2359,7 +2246,7 @@
   2.724          val init_ss = HOL_basic_ss addsimps ext_defs;
   2.725        in
   2.726          prove_standard [] surjective_prop
   2.727 -          (fn prems =>
   2.728 +          (fn _ =>
   2.729              EVERY
   2.730               [rtac surject_assist_idE 1,
   2.731                simp_tac init_ss 1,
   2.732 @@ -2369,7 +2256,7 @@
   2.733  
   2.734      fun split_meta_prf () =
   2.735        prove false [] split_meta_prop
   2.736 -        (fn prems =>
   2.737 +        (fn _ =>
   2.738            EVERY
   2.739             [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
   2.740              etac meta_allE 1, atac 1,
   2.741 @@ -2423,7 +2310,7 @@
   2.742          val so' = named_cterm_instantiate ([(P_nm, not_P)]) split_object;
   2.743          val so'' = simplify ss so';
   2.744        in
   2.745 -        prove_standard [] split_ex_prop (fn prems => resolve_tac [so''] 1)
   2.746 +        prove_standard [] split_ex_prop (fn _ => resolve_tac [so''] 1)
   2.747        end;
   2.748      val split_ex = timeit_msg "record split_ex proof:" split_ex_prf;
   2.749  
     3.1 --- a/src/Pure/Concurrent/task_queue.ML	Thu Oct 01 09:09:56 2009 +0200
     3.2 +++ b/src/Pure/Concurrent/task_queue.ML	Thu Oct 01 11:33:32 2009 +0200
     3.3 @@ -125,7 +125,7 @@
     3.4  fun status (Queue {jobs, ...}) =
     3.5    let
     3.6      val (x, y, z) =
     3.7 -      Task_Graph.fold (fn (task, ((_, job), (deps, _))) => fn (x, y, z) =>
     3.8 +      Task_Graph.fold (fn (_, ((_, job), (deps, _))) => fn (x, y, z) =>
     3.9            (case job of
    3.10              Job _ => if null deps then (x + 1, y, z) else (x, y + 1, z)
    3.11            | Running _ => (x, y, z + 1)))
     4.1 --- a/src/Pure/General/heap.ML	Thu Oct 01 09:09:56 2009 +0200
     4.2 +++ b/src/Pure/General/heap.ML	Thu Oct 01 11:33:32 2009 +0200
     4.3 @@ -78,8 +78,8 @@
     4.4  
     4.5  nonfix upto;
     4.6  
     4.7 -fun upto _ (h as Empty) = ([], h)
     4.8 -  | upto limit (h as Heap (_, x, a, b)) =
     4.9 +fun upto _ Empty = ([], Empty)
    4.10 +  | upto limit (h as Heap (_, x, _, _)) =
    4.11        (case ord (x, limit) of
    4.12          GREATER => ([], h)
    4.13        | _ => upto limit (delete_min h) |>> cons x);
     5.1 --- a/src/Pure/General/pretty.ML	Thu Oct 01 09:09:56 2009 +0200
     5.2 +++ b/src/Pure/General/pretty.ML	Thu Oct 01 11:33:32 2009 +0200
     5.3 @@ -197,11 +197,11 @@
     5.4  fun setdepth dp = (depth := dp);
     5.5  
     5.6  local
     5.7 -  fun pruning dp (Block (m, bes, indent, wd)) =
     5.8 +  fun pruning dp (Block (m, bes, indent, _)) =
     5.9          if dp > 0
    5.10          then block_markup m (indent, map (pruning (dp - 1)) bes)
    5.11          else str "..."
    5.12 -    | pruning dp e = e
    5.13 +    | pruning _ e = e;
    5.14  in
    5.15    fun prune e = if ! depth > 0 then pruning (! depth) e else e;
    5.16  end;
    5.17 @@ -219,7 +219,7 @@
    5.18    pos = 0,
    5.19    nl = 0};
    5.20  
    5.21 -fun newline {tx, ind, pos, nl} : text =
    5.22 +fun newline {tx, ind = _, pos = _, nl} : text =
    5.23   {tx = Buffer.add (Output.output "\n") tx,
    5.24    ind = Buffer.empty,
    5.25    pos = 0,
    5.26 @@ -250,22 +250,22 @@
    5.27  (*Add the lengths of the expressions until the next Break; if no Break then
    5.28    include "after", to account for text following this block.*)
    5.29  fun breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after)
    5.30 -  | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
    5.31 -  | breakdist (Break _ :: es, after) = 0
    5.32 +  | breakdist (String (_, len) :: es, after) = len + breakdist (es, after)
    5.33 +  | breakdist (Break _ :: _, _) = 0
    5.34    | breakdist ([], after) = after;
    5.35  
    5.36  (*Search for the next break (at this or higher levels) and force it to occur.*)
    5.37  fun forcenext [] = []
    5.38 -  | forcenext (Break (_, wd) :: es) = Break (true, 0) :: es
    5.39 +  | forcenext (Break _ :: es) = Break (true, 0) :: es
    5.40    | forcenext (e :: es) = e :: forcenext es;
    5.41  
    5.42  (*es is list of expressions to print;
    5.43    blockin is the indentation of the current block;
    5.44    after is the width of the following context until next break.*)
    5.45  fun format ([], _, _) text = text
    5.46 -  | format (e :: es, block as (blockind, blockin), after) (text as {ind, pos, nl, ...}) =
    5.47 +  | format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) =
    5.48        (case e of
    5.49 -        Block ((bg, en), bes, indent, wd) =>
    5.50 +        Block ((bg, en), bes, indent, _) =>
    5.51            let
    5.52              val {emergencypos, ...} = ! margin_info;
    5.53              val pos' = pos + indent;
     6.1 --- a/src/Pure/General/scan.ML	Thu Oct 01 09:09:56 2009 +0200
     6.2 +++ b/src/Pure/General/scan.ML	Thu Oct 01 11:33:32 2009 +0200
     6.3 @@ -273,7 +273,7 @@
     6.4  val empty_lexicon = Lexicon Symtab.empty;
     6.5  
     6.6  fun is_literal _ [] = false
     6.7 -  | is_literal (Lexicon tab) (chs as c :: cs) =
     6.8 +  | is_literal (Lexicon tab) (c :: cs) =
     6.9        (case Symtab.lookup tab c of
    6.10          SOME (tip, lex) => tip andalso null cs orelse is_literal lex cs
    6.11        | NONE => false);
    6.12 @@ -286,7 +286,7 @@
    6.13      fun finish (SOME (res, rest)) = (rev res, rest)
    6.14        | finish NONE = raise FAIL NONE;
    6.15      fun scan _ res (Lexicon tab) [] = if Symtab.is_empty tab then finish res else raise MORE NONE
    6.16 -      | scan path res (Lexicon tab) (chs as c :: cs) =
    6.17 +      | scan path res (Lexicon tab) (c :: cs) =
    6.18            (case Symtab.lookup tab (fst c) of
    6.19              SOME (tip, lex) =>
    6.20                let val path' = c :: path
    6.21 @@ -300,7 +300,7 @@
    6.22  fun extend_lexicon chrs lexicon =
    6.23    let
    6.24      fun ext [] lex = lex
    6.25 -      | ext (chs as c :: cs) (Lexicon tab) =
    6.26 +      | ext (c :: cs) (Lexicon tab) =
    6.27            (case Symtab.lookup tab c of
    6.28              SOME (tip, lex) => Lexicon (Symtab.update (c, (tip orelse null cs, ext cs lex)) tab)
    6.29            | NONE => Lexicon (Symtab.update (c, (null cs, ext cs empty_lexicon)) tab));
     7.1 --- a/src/Pure/General/symbol_pos.ML	Thu Oct 01 09:09:56 2009 +0200
     7.2 +++ b/src/Pure/General/symbol_pos.ML	Thu Oct 01 11:33:32 2009 +0200
     7.3 @@ -161,7 +161,7 @@
     7.4  
     7.5  fun pad [] = []
     7.6    | pad [(s, _)] = [s]
     7.7 -  | pad ((s1, pos1) :: (rest as (s2, pos2) :: _)) =
     7.8 +  | pad ((s1, pos1) :: (rest as (_, pos2) :: _)) =
     7.9        let
    7.10          val end_pos1 = Position.advance s1 pos1;
    7.11          val d = Int.max (0, Position.distance_of end_pos1 pos2);
     8.1 --- a/src/Pure/Isar/args.ML	Thu Oct 01 09:09:56 2009 +0200
     8.2 +++ b/src/Pure/Isar/args.ML	Thu Oct 01 11:33:32 2009 +0200
     8.3 @@ -283,7 +283,7 @@
     8.4  
     8.5  (** syntax wrapper **)
     8.6  
     8.7 -fun syntax kind scan (src as Src ((s, args), pos)) st =
     8.8 +fun syntax kind scan (Src ((s, args), pos)) st =
     8.9    (case Scan.error (Scan.finite' T.stopper (Scan.option scan)) (st, args) of
    8.10      (SOME x, (st', [])) => (x, st')
    8.11    | (_, (_, args')) =>
     9.1 --- a/src/Pure/Isar/context_rules.ML	Thu Oct 01 09:09:56 2009 +0200
     9.2 +++ b/src/Pure/Isar/context_rules.ML	Thu Oct 01 11:33:32 2009 +0200
     9.3 @@ -131,8 +131,8 @@
     9.4  (* retrieving rules *)
     9.5  
     9.6  fun untaglist [] = []
     9.7 -  | untaglist [(k : int * int, x)] = [x]
     9.8 -  | untaglist ((k, x) :: (rest as (k', x') :: _)) =
     9.9 +  | untaglist [(_ : int * int, x)] = [x]
    9.10 +  | untaglist ((k, x) :: (rest as (k', _) :: _)) =
    9.11        if k = k' then untaglist rest
    9.12        else x :: untaglist rest;
    9.13  
    9.14 @@ -160,7 +160,7 @@
    9.15  (* wrappers *)
    9.16  
    9.17  fun gen_add_wrapper upd w =
    9.18 -  Context.theory_map (Rules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
    9.19 +  Context.theory_map (Rules.map (fn Rules {next, rules, netpairs, wrappers} =>
    9.20      make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers)));
    9.21  
    9.22  val addSWrapper = gen_add_wrapper Library.apfst;
    10.1 --- a/src/Pure/Isar/expression.ML	Thu Oct 01 09:09:56 2009 +0200
    10.2 +++ b/src/Pure/Isar/expression.ML	Thu Oct 01 11:33:32 2009 +0200
    10.3 @@ -311,7 +311,7 @@
    10.4    | finish_primitive _ close (Defines defs) = close (Defines defs)
    10.5    | finish_primitive _ _ (Notes facts) = Notes facts;
    10.6  
    10.7 -fun finish_inst ctxt parms do_close (loc, (prfx, inst)) =
    10.8 +fun finish_inst ctxt (loc, (prfx, inst)) =
    10.9    let
   10.10      val thy = ProofContext.theory_of ctxt;
   10.11      val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
   10.12 @@ -323,7 +323,7 @@
   10.13  
   10.14  fun finish ctxt parms do_close insts elems =
   10.15    let
   10.16 -    val deps = map (finish_inst ctxt parms do_close) insts;
   10.17 +    val deps = map (finish_inst ctxt) insts;
   10.18      val elems' = map (finish_elem ctxt parms do_close) elems;
   10.19    in (deps, elems') end;
   10.20  
    11.1 --- a/src/Pure/Isar/isar_document.ML	Thu Oct 01 09:09:56 2009 +0200
    11.2 +++ b/src/Pure/Isar/isar_document.ML	Thu Oct 01 11:33:32 2009 +0200
    11.3 @@ -13,6 +13,7 @@
    11.4    val begin_document: document_id -> Path.T -> unit
    11.5    val end_document: document_id -> unit
    11.6    val edit_document: document_id -> document_id -> (command_id * command_id option) list -> unit
    11.7 +  val init: unit -> unit
    11.8  end;
    11.9  
   11.10  structure Isar_Document: ISAR_DOCUMENT =
    12.1 --- a/src/Pure/Isar/obtain.ML	Thu Oct 01 09:09:56 2009 +0200
    12.2 +++ b/src/Pure/Isar/obtain.ML	Thu Oct 01 11:33:32 2009 +0200
    12.3 @@ -215,7 +215,6 @@
    12.4      val thy = ProofContext.theory_of ctxt;
    12.5      val certT = Thm.ctyp_of thy;
    12.6      val cert = Thm.cterm_of thy;
    12.7 -    val string_of_typ = Syntax.string_of_typ ctxt;
    12.8      val string_of_term = setmp show_types true (Syntax.string_of_term ctxt);
    12.9  
   12.10      fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th);
    13.1 --- a/src/Pure/Isar/proof.ML	Thu Oct 01 09:09:56 2009 +0200
    13.2 +++ b/src/Pure/Isar/proof.ML	Thu Oct 01 11:33:32 2009 +0200
    13.3 @@ -581,7 +581,6 @@
    13.4    let
    13.5      val _ = assert_forward state;
    13.6      val thy = theory_of state;
    13.7 -    val ctxt = context_of state;
    13.8  
    13.9      val (raw_name_atts, (raw_vars, raw_rhss)) = args |> split_list ||> split_list;
   13.10      val name_atts = map (apsnd (map (prep_att thy))) raw_name_atts;
   13.11 @@ -1008,7 +1007,7 @@
   13.12    let
   13.13      val _ = assert_backward state;
   13.14      val (goal_ctxt, (_, goal)) = find_goal state;
   13.15 -    val {statement as (kind, propss, prop), messages, using, goal, before_qed, after_qed} = goal;
   13.16 +    val {statement as (kind, _, prop), messages, using, goal, before_qed, after_qed} = goal;
   13.17      val goal_txt = prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt);
   13.18  
   13.19      val _ = is_relevant state andalso error "Cannot fork relevant proof";
    14.1 --- a/src/Pure/Isar/proof_context.ML	Thu Oct 01 09:09:56 2009 +0200
    14.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Oct 01 11:33:32 2009 +0200
    14.3 @@ -1033,7 +1033,7 @@
    14.4  
    14.5  local
    14.6  
    14.7 -fun const_syntax ctxt (Free (x, T), mx) = SOME (true, (x, T, mx))
    14.8 +fun const_syntax _ (Free (x, T), mx) = SOME (true, (x, T, mx))
    14.9    | const_syntax ctxt (Const (c, _), mx) =
   14.10        Option.map (pair false) (try (Consts.syntax (consts_of ctxt)) (c, mx))
   14.11    | const_syntax _ _ = NONE;
   14.12 @@ -1106,7 +1106,7 @@
   14.13  
   14.14  (* fixes vs. frees *)
   14.15  
   14.16 -fun auto_fixes (arg as (ctxt, (propss, x))) =
   14.17 +fun auto_fixes (ctxt, (propss, x)) =
   14.18    ((fold o fold) Variable.auto_fixes propss ctxt, (propss, x));
   14.19  
   14.20  fun bind_fixes xs ctxt =
    15.1 --- a/src/Pure/Isar/proof_node.ML	Thu Oct 01 09:09:56 2009 +0200
    15.2 +++ b/src/Pure/Isar/proof_node.ML	Thu Oct 01 11:33:32 2009 +0200
    15.3 @@ -41,7 +41,7 @@
    15.4  
    15.5  (* apply transformer *)
    15.6  
    15.7 -fun applys f (ProofNode (node as (st, _), n)) =
    15.8 +fun applys f (ProofNode ((st, _), n)) =
    15.9    (case Seq.pull (f st) of
   15.10      NONE => error "empty result sequence -- proof command failed"
   15.11    | SOME res => ProofNode (res, n + 1));
    16.1 --- a/src/Pure/Isar/rule_insts.ML	Thu Oct 01 09:09:56 2009 +0200
    16.2 +++ b/src/Pure/Isar/rule_insts.ML	Thu Oct 01 11:33:32 2009 +0200
    16.3 @@ -266,8 +266,8 @@
    16.4    let
    16.5      val thy = ProofContext.theory_of ctxt;
    16.6      (* Separate type and term insts *)
    16.7 -    fun has_type_var ((x, _), _) = (case Symbol.explode x of
    16.8 -          "'"::cs => true | cs => false);
    16.9 +    fun has_type_var ((x, _), _) =
   16.10 +      (case Symbol.explode x of "'" :: _ => true | _ => false);
   16.11      val Tinsts = List.filter has_type_var insts;
   16.12      val tinsts = filter_out has_type_var insts;
   16.13  
    17.1 --- a/src/Pure/Isar/specification.ML	Thu Oct 01 09:09:56 2009 +0200
    17.2 +++ b/src/Pure/Isar/specification.ML	Thu Oct 01 11:33:32 2009 +0200
    17.3 @@ -136,9 +136,6 @@
    17.4    prepare prep_vars parse_prop prep_att do_close
    17.5      vars (map single_spec specs) #>> apsnd (map the_spec);
    17.6  
    17.7 -fun prep_specification prep_vars parse_prop prep_att vars specs =
    17.8 -  prepare prep_vars parse_prop prep_att true [specs];
    17.9 -
   17.10  in
   17.11  
   17.12  fun check_spec x = prep_spec ProofContext.cert_vars (K I) (K I) true x;
    18.1 --- a/src/Pure/Isar/theory_target.ML	Thu Oct 01 09:09:56 2009 +0200
    18.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Oct 01 11:33:32 2009 +0200
    18.3 @@ -45,7 +45,7 @@
    18.4  
    18.5  (* pretty *)
    18.6  
    18.7 -fun pretty_thy ctxt target is_locale is_class =
    18.8 +fun pretty_thy ctxt target is_class =
    18.9    let
   18.10      val thy = ProofContext.theory_of ctxt;
   18.11      val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
   18.12 @@ -63,12 +63,12 @@
   18.13        (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)]
   18.14    end;
   18.15  
   18.16 -fun pretty (Target {target, is_locale, is_class, instantiation, overloading, ...}) ctxt =
   18.17 +fun pretty (Target {target, is_class, instantiation, overloading, ...}) ctxt =
   18.18    Pretty.block [Pretty.str "theory", Pretty.brk 1,
   18.19        Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] ::
   18.20      (if not (null overloading) then [Overloading.pretty ctxt]
   18.21       else if not (null (#1 instantiation)) then [Class_Target.pretty_instantiation ctxt]
   18.22 -     else pretty_thy ctxt target is_locale is_class);
   18.23 +     else pretty_thy ctxt target is_class);
   18.24  
   18.25  
   18.26  (* target declarations *)
   18.27 @@ -260,8 +260,7 @@
   18.28  
   18.29  (* define *)
   18.30  
   18.31 -fun define (ta as Target {target, is_locale, is_class, ...})
   18.32 -    kind ((b, mx), ((name, atts), rhs)) lthy =
   18.33 +fun define ta kind ((b, mx), ((name, atts), rhs)) lthy =
   18.34    let
   18.35      val thy = ProofContext.theory_of lthy;
   18.36      val thy_ctxt = ProofContext.init thy;
    19.1 --- a/src/Pure/Isar/toplevel.ML	Thu Oct 01 09:09:56 2009 +0200
    19.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Oct 01 11:33:32 2009 +0200
    19.3 @@ -126,7 +126,6 @@
    19.4    SkipProof of int * (generic_theory * generic_theory);
    19.5      (*proof depth, resulting theory, original theory*)
    19.6  
    19.7 -val the_global_theory = fn Theory (Context.Theory thy, _) => thy | _ => raise UNDEF;
    19.8  val theory_node = fn Theory (gthy, _) => SOME gthy | _ => NONE;
    19.9  val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE;
   19.10  
   19.11 @@ -256,7 +255,7 @@
   19.12  
   19.13  in
   19.14  
   19.15 -fun apply_transaction pos f g (node, exit) =
   19.16 +fun apply_transaction f g (node, exit) =
   19.17    let
   19.18      val _ = is_draft_theory node andalso error "Illegal draft theory in toplevel state";
   19.19      val cont_node = reset_presentation node;
   19.20 @@ -293,29 +292,29 @@
   19.21  
   19.22  local
   19.23  
   19.24 -fun apply_tr int _ (Init (_, f, exit)) (State (NONE, _)) =
   19.25 +fun apply_tr int (Init (_, f, exit)) (State (NONE, _)) =
   19.26        State (SOME (Theory (Context.Theory (Theory.checkpoint (f int)), NONE), exit), NONE)
   19.27 -  | apply_tr _ _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) =
   19.28 +  | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) =
   19.29        State (NONE, prev)
   19.30 -  | apply_tr _ _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =
   19.31 +  | apply_tr _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =
   19.32        (Runtime.controlled_execution exit thy; toplevel)
   19.33 -  | apply_tr int _ (Keep f) state =
   19.34 +  | apply_tr int (Keep f) state =
   19.35        Runtime.controlled_execution (fn x => tap (f int) x) state
   19.36 -  | apply_tr int pos (Transaction (f, g)) (State (SOME state, _)) =
   19.37 -      apply_transaction pos (fn x => f int x) g state
   19.38 -  | apply_tr _ _ _ _ = raise UNDEF;
   19.39 +  | apply_tr int (Transaction (f, g)) (State (SOME state, _)) =
   19.40 +      apply_transaction (fn x => f int x) g state
   19.41 +  | apply_tr _ _ _ = raise UNDEF;
   19.42  
   19.43 -fun apply_union _ _ [] state = raise FAILURE (state, UNDEF)
   19.44 -  | apply_union int pos (tr :: trs) state =
   19.45 -      apply_union int pos trs state
   19.46 -        handle Runtime.UNDEF => apply_tr int pos tr state
   19.47 -          | FAILURE (alt_state, UNDEF) => apply_tr int pos tr alt_state
   19.48 +fun apply_union _ [] state = raise FAILURE (state, UNDEF)
   19.49 +  | apply_union int (tr :: trs) state =
   19.50 +      apply_union int trs state
   19.51 +        handle Runtime.UNDEF => apply_tr int tr state
   19.52 +          | FAILURE (alt_state, UNDEF) => apply_tr int tr alt_state
   19.53            | exn as FAILURE _ => raise exn
   19.54            | exn => raise FAILURE (state, exn);
   19.55  
   19.56  in
   19.57  
   19.58 -fun apply_trans int pos trs state = (apply_union int pos trs state, NONE)
   19.59 +fun apply_trans int trs state = (apply_union int trs state, NONE)
   19.60    handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn);
   19.61  
   19.62  end;
   19.63 @@ -562,14 +561,14 @@
   19.64  
   19.65  local
   19.66  
   19.67 -fun app int (tr as Transition {trans, pos, print, no_timing, ...}) =
   19.68 +fun app int (tr as Transition {trans, print, no_timing, ...}) =
   19.69    setmp_thread_position tr (fn state =>
   19.70      let
   19.71        fun do_timing f x = (warning (command_msg "" tr); timeap f x);
   19.72        fun do_profiling f x = profile (! profiling) f x;
   19.73  
   19.74        val (result, status) =
   19.75 -         state |> (apply_trans int pos trans
   19.76 +         state |> (apply_trans int trans
   19.77            |> (if ! profiling > 0 andalso not no_timing then do_profiling else I)
   19.78            |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I));
   19.79  
    20.1 --- a/src/Pure/Isar/value_parse.ML	Thu Oct 01 09:09:56 2009 +0200
    20.2 +++ b/src/Pure/Isar/value_parse.ML	Thu Oct 01 11:33:32 2009 +0200
    20.3 @@ -9,6 +9,7 @@
    20.4    val comma: 'a parser -> 'a parser
    20.5    val equal: 'a parser -> 'a parser
    20.6    val parens: 'a parser -> 'a parser
    20.7 +  val unit: unit parser
    20.8    val pair: 'a parser -> 'b parser -> ('a * 'b) parser
    20.9    val triple: 'a parser -> 'b parser -> 'c parser -> ('a * 'b * 'c) parser
   20.10    val list: 'a parser -> 'a list parser
    21.1 --- a/src/Pure/ML/ml_antiquote.ML	Thu Oct 01 09:09:56 2009 +0200
    21.2 +++ b/src/Pure/ML/ml_antiquote.ML	Thu Oct 01 11:33:32 2009 +0200
    21.3 @@ -41,7 +41,7 @@
    21.4      (Context.Proof ctxt, fn {background, ...} => (K ("", ""), background)))));
    21.5  
    21.6  fun inline name scan = ML_Context.add_antiq name
    21.7 -  (fn _ => scan >> (fn s => fn {struct_name, background} => (K ("", s), background)));
    21.8 +  (fn _ => scan >> (fn s => fn {background, ...} => (K ("", s), background)));
    21.9  
   21.10  fun declaration kind name scan = ML_Context.add_antiq name
   21.11    (fn _ => scan >> (fn s => fn {struct_name, background} =>
    22.1 --- a/src/Pure/Proof/extraction.ML	Thu Oct 01 09:09:56 2009 +0200
    22.2 +++ b/src/Pure/Proof/extraction.ML	Thu Oct 01 11:33:32 2009 +0200
    22.3 @@ -81,8 +81,7 @@
    22.4    {next = next - 1, rs = r :: rs, net = Net.insert_term (K false)
    22.5       (Envir.eta_contract lhs, (next, r)) net};
    22.6  
    22.7 -fun merge_rules
    22.8 -  ({next, rs = rs1, net} : rules) ({next = next2, rs = rs2, ...} : rules) =
    22.9 +fun merge_rules ({next, rs = rs1, net} : rules) ({rs = rs2, ...} : rules) =
   22.10    List.foldr add_rule {next = next, rs = rs1, net = net} (subtract (op =) rs1 rs2);
   22.11  
   22.12  fun condrew thy rules procs =
   22.13 @@ -141,7 +140,7 @@
   22.14    map_proof_terms (subst_TVars tye) (typ_subst_TVars tye);
   22.15  
   22.16  fun relevant_vars types prop = List.foldr (fn
   22.17 -      (Var ((a, i), T), vs) => (case strip_type T of
   22.18 +      (Var ((a, _), T), vs) => (case strip_type T of
   22.19          (_, Type (s, _)) => if member (op =) types s then a :: vs else vs
   22.20        | _ => vs)
   22.21      | (_, vs) => vs) [] (vars_of prop);
    23.1 --- a/src/Pure/Syntax/ast.ML	Thu Oct 01 09:09:56 2009 +0200
    23.2 +++ b/src/Pure/Syntax/ast.ML	Thu Oct 01 11:33:32 2009 +0200
    23.3 @@ -94,7 +94,7 @@
    23.4  
    23.5  (** check translation rules **)
    23.6  
    23.7 -fun rule_error (rule as (lhs, rhs)) =
    23.8 +fun rule_error (lhs, rhs) =
    23.9    let
   23.10      fun add_vars (Constant _) = I
   23.11        | add_vars (Variable x) = cons x
    24.1 --- a/src/Pure/Syntax/mixfix.ML	Thu Oct 01 09:09:56 2009 +0200
    24.2 +++ b/src/Pure/Syntax/mixfix.ML	Thu Oct 01 11:33:32 2009 +0200
    24.3 @@ -128,16 +128,6 @@
    24.4  
    24.5  fun const_mixfix c mx = (const_name mx c, fix_mixfix c mx);
    24.6  
    24.7 -fun map_mixfix _ NoSyn = NoSyn
    24.8 -  | map_mixfix f (Mixfix (sy, ps, p)) = Mixfix (f sy, ps, p)
    24.9 -  | map_mixfix f (Delimfix sy) = Delimfix (f sy)
   24.10 -  | map_mixfix f (InfixName (sy, p)) = InfixName (f sy, p)
   24.11 -  | map_mixfix f (InfixlName (sy, p)) = InfixlName (f sy, p)
   24.12 -  | map_mixfix f (InfixrName (sy, p)) = InfixrName (f sy, p)
   24.13 -  | map_mixfix f (Binder (sy, p, q)) = Binder (f sy, p, q)
   24.14 -  | map_mixfix _ Structure = Structure
   24.15 -  | map_mixfix _ _ = raise Fail ("map_mixfix: illegal occurrence of unnamed infix");
   24.16 -
   24.17  fun mixfix_args NoSyn = 0
   24.18    | mixfix_args (Mixfix (sy, _, _)) = SynExt.mfix_args sy
   24.19    | mixfix_args (Delimfix sy) = SynExt.mfix_args sy
    25.1 --- a/src/Pure/Syntax/syn_ext.ML	Thu Oct 01 09:09:56 2009 +0200
    25.2 +++ b/src/Pure/Syntax/syn_ext.ML	Thu Oct 01 11:33:32 2009 +0200
    25.3 @@ -270,9 +270,9 @@
    25.4      fun rem_pri (Argument (s, _)) = Argument (s, chain_pri)
    25.5        | rem_pri sym = sym;
    25.6  
    25.7 -    fun logify_types copy_prod (a as (Argument (s, p))) =
    25.8 +    fun logify_types (a as (Argument (s, p))) =
    25.9            if s <> "prop" andalso is_logtype s then Argument (logic, p) else a
   25.10 -      | logify_types _ a = a;
   25.11 +      | logify_types a = a;
   25.12  
   25.13  
   25.14      val raw_symbs = read_mfix sy handle ERROR msg => err_in_mfix msg mfix;
   25.15 @@ -305,7 +305,7 @@
   25.16        if convert andalso not copy_prod then
   25.17         (if lhs = "prop" then sprop else if is_logtype lhs then logic else lhs)
   25.18        else lhs;
   25.19 -    val symbs' = map (logify_types copy_prod) symbs;
   25.20 +    val symbs' = map logify_types symbs;
   25.21      val xprod = XProd (lhs', symbs', const', pri);
   25.22  
   25.23      val _ = (List.app check_pri pris; check_pri pri; check_blocks symbs');
    26.1 --- a/src/Pure/Syntax/syn_trans.ML	Thu Oct 01 09:09:56 2009 +0200
    26.2 +++ b/src/Pure/Syntax/syn_trans.ML	Thu Oct 01 11:33:32 2009 +0200
    26.3 @@ -155,20 +155,11 @@
    26.4    | bigimpl_ast_tr (*"_bigimpl"*) asts = raise Ast.AST ("bigimpl_ast_tr", asts);
    26.5  
    26.6  
    26.7 -(* meta conjunction *)
    26.8 -
    26.9 -fun conjunction_tr [t, u] = Lexicon.const "Pure.conjunction" $ t $ u
   26.10 -  | conjunction_tr ts = raise TERM ("conjunction_tr", ts);
   26.11 -
   26.12 -
   26.13  (* type/term reflection *)
   26.14  
   26.15  fun type_tr (*"_TYPE"*) [ty] = mk_type ty
   26.16    | type_tr (*"_TYPE"*) ts = raise TERM ("type_tr", ts);
   26.17  
   26.18 -fun term_tr [t] = Lexicon.const "Pure.term" $ t
   26.19 -  | term_tr ts = raise TERM ("term_tr", ts);
   26.20 -
   26.21  
   26.22  (* dddot *)
   26.23  
    27.1 --- a/src/Pure/Syntax/syntax.ML	Thu Oct 01 09:09:56 2009 +0200
    27.2 +++ b/src/Pure/Syntax/syntax.ML	Thu Oct 01 11:33:32 2009 +0200
    27.3 @@ -404,7 +404,7 @@
    27.4  
    27.5  fun pretty_gram (Syntax (tabs, _)) =
    27.6    let
    27.7 -    val {lexicon, prmodes, gram, prtabs, ...} = tabs;
    27.8 +    val {lexicon, prmodes, gram, ...} = tabs;
    27.9      val prmodes' = sort_strings (filter_out (fn s => s = "") prmodes);
   27.10    in
   27.11      [pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon),
   27.12 @@ -639,7 +639,7 @@
   27.13  
   27.14  local
   27.15  
   27.16 -fun unparse_t t_to_ast prt_t markup ctxt (syn as Syntax (tabs, _)) curried t =
   27.17 +fun unparse_t t_to_ast prt_t markup ctxt (Syntax (tabs, _)) curried t =
   27.18    let
   27.19      val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
   27.20      val ast = t_to_ast ctxt (lookup_tr' print_trtab) t;
    28.1 --- a/src/Pure/Syntax/type_ext.ML	Thu Oct 01 09:09:56 2009 +0200
    28.2 +++ b/src/Pure/Syntax/type_ext.ML	Thu Oct 01 11:33:32 2009 +0200
    28.3 @@ -82,8 +82,8 @@
    28.4            if Lexicon.is_tid x then TFree (x, get_sort (x, ~1))
    28.5            else Type (x, [])
    28.6        | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
    28.7 -      | typ_of (Const ("_tfree",_) $ (t as Free x)) = typ_of t
    28.8 -      | typ_of (Const ("_tvar",_) $ (t as Var x)) = typ_of t
    28.9 +      | typ_of (Const ("_tfree",_) $ (t as Free _)) = typ_of t
   28.10 +      | typ_of (Const ("_tvar",_) $ (t as Var _)) = typ_of t
   28.11        | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1))
   28.12        | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) =
   28.13            TFree (x, get_sort (x, ~1))
    29.1 --- a/src/Pure/System/isabelle_process.ML	Thu Oct 01 09:09:56 2009 +0200
    29.2 +++ b/src/Pure/System/isabelle_process.ML	Thu Oct 01 11:33:32 2009 +0200
    29.3 @@ -133,6 +133,7 @@
    29.4   (Unsynchronized.change print_mode (update (op =) isabelle_processN);
    29.5    setup_channels out |> init_message;
    29.6    OuterKeyword.report ();
    29.7 +  Isar_Document.init ();
    29.8    Output.status (Markup.markup Markup.ready "");
    29.9    Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
   29.10  
    30.1 --- a/src/Pure/System/isar.ML	Thu Oct 01 09:09:56 2009 +0200
    30.2 +++ b/src/Pure/System/isar.ML	Thu Oct 01 11:33:32 2009 +0200
    30.3 @@ -48,7 +48,6 @@
    30.4    in edit count (! global_state, ! global_history) end);
    30.5  
    30.6  fun state () = NAMED_CRITICAL "Isar" (fn () => ! global_state);
    30.7 -fun set_state state = NAMED_CRITICAL "Isar" (fn () => global_state := state);
    30.8  
    30.9  fun exn () = NAMED_CRITICAL "Isar" (fn () => ! global_exn);
   30.10  fun set_exn exn =  NAMED_CRITICAL "Isar" (fn () => global_exn := exn);
    31.1 --- a/src/Pure/Thy/html.ML	Thu Oct 01 09:09:56 2009 +0200
    31.2 +++ b/src/Pure/Thy/html.ML	Thu Oct 01 11:33:32 2009 +0200
    31.3 @@ -222,7 +222,6 @@
    31.4      in (implode syms, width) end;
    31.5  
    31.6  val output = #1 o output_width;
    31.7 -val output_symbols = map #2 o output_syms;
    31.8  
    31.9  val _ = Output.add_mode htmlN output_width Symbol.encode_raw;
   31.10  
    32.1 --- a/src/Pure/Thy/thy_info.ML	Thu Oct 01 09:09:56 2009 +0200
    32.2 +++ b/src/Pure/Thy/thy_info.ML	Thu Oct 01 11:33:32 2009 +0200
    32.3 @@ -283,7 +283,7 @@
    32.4  
    32.5  local
    32.6  
    32.7 -fun provide path name info (deps as SOME {update_time, master, text, parents, files}) =
    32.8 +fun provide path name info (SOME {update_time, master, text, parents, files}) =
    32.9       (if AList.defined (op =) files path then ()
   32.10        else warning (loader_msg "undeclared dependency of theory" [name] ^
   32.11          " on file: " ^ quote (Path.implode path));
   32.12 @@ -338,7 +338,7 @@
   32.13  fun load_thy time upd_time initiators name =
   32.14    let
   32.15      val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
   32.16 -    val (pos, text, files) =
   32.17 +    val (pos, text, _) =
   32.18        (case get_deps name of
   32.19          SOME {master = SOME (master_path, _), text as _ :: _, files, ...} =>
   32.20            (Path.position master_path, text, files)
   32.21 @@ -410,7 +410,7 @@
   32.22  
   32.23  in
   32.24  
   32.25 -fun schedule_tasks tasks n =
   32.26 +fun schedule_tasks tasks =
   32.27    if not (Multithreading.enabled ()) then schedule_seq tasks
   32.28    else if Multithreading.self_critical () then
   32.29       (warning (loader_msg "no multithreading within critical section" []);
   32.30 @@ -438,7 +438,7 @@
   32.31    | NONE =>
   32.32        let val {master, text, imports = parents, uses = files} = ThyLoad.deps_thy dir name
   32.33        in (false, init_deps (SOME master) text parents files, parents) end
   32.34 -  | SOME (deps as SOME {update_time, master, text, parents, files}) =>
   32.35 +  | SOME (SOME {update_time, master, text, parents, files}) =>
   32.36        let
   32.37          val (thy_path, thy_id) = ThyLoad.check_thy dir name;
   32.38          val master' = SOME (thy_path, thy_id);
   32.39 @@ -471,7 +471,7 @@
   32.40      val dir' = Path.append dir (Path.dir path);
   32.41      val _ = member (op =) initiators name andalso error (cycle_msg initiators);
   32.42    in
   32.43 -    (case try (Graph.get_node (fst tasks)) name of
   32.44 +    (case try (Graph.get_node tasks) name of
   32.45        SOME task => (task_finished task, tasks)
   32.46      | NONE =>
   32.47          let
   32.48 @@ -481,7 +481,7 @@
   32.49                  required_by "\n" initiators);
   32.50            val parent_names = map base_name parents;
   32.51  
   32.52 -          val (parents_current, (tasks_graph', tasks_len')) =
   32.53 +          val (parents_current, tasks_graph') =
   32.54              require_thys time (name :: initiators)
   32.55                (Path.append dir (master_dir' deps)) parents tasks;
   32.56  
   32.57 @@ -496,8 +496,7 @@
   32.58            val tasks_graph'' = tasks_graph' |> new_deps name parent_names
   32.59             (if all_current then Finished
   32.60              else Task (fn () => load_thy time upd_time initiators name));
   32.61 -          val tasks_len'' = if all_current then tasks_len' else tasks_len' + 1;
   32.62 -        in (all_current, (tasks_graph'', tasks_len'')) end)
   32.63 +        in (all_current, tasks_graph'') end)
   32.64    end;
   32.65  
   32.66  end;
   32.67 @@ -508,8 +507,7 @@
   32.68  local
   32.69  
   32.70  fun gen_use_thy' req dir arg =
   32.71 -  let val (_, (tasks, n)) = req [] dir arg (Graph.empty, 0)
   32.72 -  in schedule_tasks tasks n end;
   32.73 +  schedule_tasks (snd (req [] dir arg Graph.empty));
   32.74  
   32.75  fun gen_use_thy req str =
   32.76    let val name = base_name str in
    33.1 --- a/src/Pure/Tools/find_consts.ML	Thu Oct 01 09:09:56 2009 +0200
    33.2 +++ b/src/Pure/Tools/find_consts.ML	Thu Oct 01 11:33:32 2009 +0200
    33.3 @@ -107,7 +107,7 @@
    33.4                  val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
    33.5                  val sub_size =
    33.6                    Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0;
    33.7 -              in SOME sub_size end handle MATCH => NONE
    33.8 +              in SOME sub_size end handle Type.TYPE_MATCH => NONE
    33.9            end
   33.10        | make_match (Loose arg) =
   33.11            check_const (matches_subtype thy (make_pattern arg) o snd)
    34.1 --- a/src/Pure/Tools/find_theorems.ML	Thu Oct 01 09:09:56 2009 +0200
    34.2 +++ b/src/Pure/Tools/find_theorems.ML	Thu Oct 01 11:33:32 2009 +0200
    34.3 @@ -76,18 +76,9 @@
    34.4  
    34.5  fun is_nontrivial thy = Term.is_Const o Term.head_of o ObjectLogic.drop_judgment thy;
    34.6  
    34.7 -(* Note: ("op =" : "bool --> bool --> bool") does not exist in Pure. *)
    34.8 -fun is_Iff c =
    34.9 -  (case dest_Const c of
   34.10 -     ("op =", ty) =>
   34.11 -       (ty
   34.12 -        |> strip_type
   34.13 -        |> swap
   34.14 -        |> (op ::)
   34.15 -        |> map (fst o dest_Type)
   34.16 -        |> forall (curry (op =) "bool")
   34.17 -        handle TYPE _ => false)
   34.18 -   | _ => false);
   34.19 +(*educated guesses on HOL*)  (* FIXME broken *)
   34.20 +val boolT = Type ("bool", []);
   34.21 +val iff_const = Const ("op =", boolT --> boolT --> boolT);
   34.22  
   34.23  (*extract terms from term_src, refine them to the parts that concern us,
   34.24    if po try match them against obj else vice versa.
   34.25 @@ -97,19 +88,20 @@
   34.26    let
   34.27      val thy = ProofContext.theory_of ctxt;
   34.28  
   34.29 -    val chkmatch = obj |> (if po then rpair else pair) #> Pattern.matches thy;
   34.30 +    fun check_match pat = Pattern.matches thy (if po then (pat, obj) else (obj, pat));
   34.31      fun matches pat =
   34.32        let
   34.33          val jpat = ObjectLogic.drop_judgment thy pat;
   34.34          val c = Term.head_of jpat;
   34.35          val pats =
   34.36            if Term.is_Const c
   34.37 -          then if doiff andalso is_Iff c
   34.38 -               then pat :: map (ObjectLogic.ensure_propT thy) ((snd o strip_comb) jpat)
   34.39 -                    |> filter (is_nontrivial thy)
   34.40 -               else [pat]
   34.41 +          then
   34.42 +            if doiff andalso c = iff_const then
   34.43 +              (pat :: map (ObjectLogic.ensure_propT thy) (snd (strip_comb jpat)))
   34.44 +                |> filter (is_nontrivial thy)
   34.45 +            else [pat]
   34.46            else [];
   34.47 -      in filter chkmatch pats end;
   34.48 +      in filter check_match pats end;
   34.49  
   34.50      fun substsize pat =
   34.51        let val (_, subst) =
   34.52 @@ -117,12 +109,11 @@
   34.53        in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end;
   34.54  
   34.55      fun bestmatch [] = NONE
   34.56 -     |  bestmatch xs = SOME (foldr1 Int.min xs);
   34.57 +      | bestmatch xs = SOME (foldr1 Int.min xs);
   34.58  
   34.59      val match_thm = matches o refine_term;
   34.60    in
   34.61 -    map match_thm (extract_terms term_src)
   34.62 -    |> flat
   34.63 +    maps match_thm (extract_terms term_src)
   34.64      |> map substsize
   34.65      |> bestmatch
   34.66    end;
   34.67 @@ -178,8 +169,8 @@
   34.68          is_matching_thm false (single, I) ctxt true (goal_tree prem) rule_tree;
   34.69        val successful = prems |> map_filter try_subst;
   34.70      in
   34.71 -    (*elim rules always have assumptions, so an elim with one
   34.72 -      assumption is as good as an intro rule with none*)
   34.73 +      (*elim rules always have assumptions, so an elim with one
   34.74 +        assumption is as good as an intro rule with none*)
   34.75        if is_nontrivial (ProofContext.theory_of ctxt) (Thm.major_prem_of thm)
   34.76          andalso not (null successful)
   34.77        then SOME (Thm.nprems_of thm - 1, foldr1 Int.min successful) else NONE
   34.78 @@ -190,15 +181,13 @@
   34.79  
   34.80  fun filter_solves ctxt goal =
   34.81    let
   34.82 -    val baregoal = Logic.get_goal (Thm.prop_of goal) 1;
   34.83 -
   34.84      fun etacn thm i = Seq.take (! tac_limit) o etac thm i;
   34.85      fun try_thm thm =
   34.86        if Thm.no_prems thm then rtac thm 1 goal
   34.87        else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
   34.88    in
   34.89      fn (_, thm) =>
   34.90 -      if (is_some o Seq.pull o try_thm) thm
   34.91 +      if is_some (Seq.pull (try_thm thm))
   34.92        then SOME (Thm.nprems_of thm, 0) else NONE
   34.93    end;
   34.94  
   34.95 @@ -218,7 +207,7 @@
   34.96  
   34.97  (* filter_pattern *)
   34.98  
   34.99 -fun get_names t = (Term.add_const_names t []) union (Term.add_free_names t []);
  34.100 +fun get_names t = Term.add_const_names t (Term.add_free_names t []);
  34.101  fun get_thm_names (_, thm) = get_names (Thm.full_prop_of thm);
  34.102  
  34.103  (*Including all constants and frees is only sound because
  34.104 @@ -238,10 +227,9 @@
  34.105  
  34.106      fun check (t, NONE) = check (t, SOME (get_thm_names t))
  34.107        | check ((_, thm), c as SOME thm_consts) =
  34.108 -          (if pat_consts subset_string thm_consts
  34.109 -              andalso (Pattern.matches_subterm (ProofContext.theory_of ctxt)
  34.110 -                                               (pat, Thm.full_prop_of thm))
  34.111 -           then SOME (0, 0) else NONE, c);
  34.112 +         (if pat_consts subset_string thm_consts andalso
  34.113 +            Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, Thm.full_prop_of thm)
  34.114 +          then SOME (0, 0) else NONE, c);
  34.115    in check end;
  34.116  
  34.117  
  34.118 @@ -253,7 +241,6 @@
  34.119    error ("Current goal required for " ^ c ^ " search criterion");
  34.120  
  34.121  val fix_goal = Thm.prop_of;
  34.122 -val fix_goalo = Option.map fix_goal;
  34.123  
  34.124  fun filter_crit _ _ (Name name) = apfst (filter_name name)
  34.125    | filter_crit _ NONE Intro = err_no_goal "intro"
  34.126 @@ -276,7 +263,7 @@
  34.127  fun app_filters thm =
  34.128    let
  34.129      fun app (NONE, _, _) = NONE
  34.130 -      | app (SOME v, consts, []) = SOME (v, thm)
  34.131 +      | app (SOME v, _, []) = SOME (v, thm)
  34.132        | app (r, consts, f :: fs) =
  34.133            let val (r', consts') = f (thm, consts)
  34.134            in app (opt_add r r', consts', fs) end;
  34.135 @@ -439,6 +426,7 @@
  34.136    end;
  34.137  
  34.138  
  34.139 +
  34.140  (** command syntax **)
  34.141  
  34.142  fun find_theorems_cmd ((opt_lim, rem_dups), spec) =
    35.1 --- a/src/Pure/axclass.ML	Thu Oct 01 09:09:56 2009 +0200
    35.2 +++ b/src/Pure/axclass.ML	Thu Oct 01 11:33:32 2009 +0200
    35.3 @@ -150,7 +150,6 @@
    35.4    let val params = #2 (get_axclasses thy);
    35.5    in fold (fn (x, c) => if pred c then cons x else I) params [] end;
    35.6  
    35.7 -fun params_of thy c = get_params thy (fn c' => c' = c);
    35.8  fun all_params_of thy S = get_params thy (fn c => Sign.subsort thy (S, [c]));
    35.9  
   35.10  fun class_of_param thy = AList.lookup (op =) (#2 (get_axclasses thy));
   35.11 @@ -263,7 +262,8 @@
   35.12  
   35.13  fun unoverload_const thy (c_ty as (c, _)) =
   35.14    case class_of_param thy c
   35.15 -   of SOME class => (case get_inst_tyco (Sign.consts_of thy) c_ty
   35.16 +   of SOME class (* FIXME unused? *) =>
   35.17 +     (case get_inst_tyco (Sign.consts_of thy) c_ty
   35.18         of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
   35.19          | NONE => c)
   35.20      | NONE => c;
   35.21 @@ -585,7 +585,7 @@
   35.22          val hyps = vars
   35.23            |> map (fn (T, S) => (T, Thm.of_sort (certT T, S) ~~ S));
   35.24          val ths = (typ, sort)
   35.25 -          |> Sorts.of_sort_derivation (Syntax.pp_global thy) (Sign.classes_of thy)
   35.26 +          |> Sorts.of_sort_derivation (Sign.classes_of thy)
   35.27             {class_relation =
   35.28                fn (th, c1) => fn c2 => th RS the_classrel thy (c1, c2),
   35.29              type_constructor =
    36.1 --- a/src/Pure/consts.ML	Thu Oct 01 09:09:56 2009 +0200
    36.2 +++ b/src/Pure/consts.ML	Thu Oct 01 11:33:32 2009 +0200
    36.3 @@ -199,7 +199,7 @@
    36.4  
    36.5  fun subscript (Type (_, Ts)) (i :: is) = subscript (nth Ts i) is
    36.6    | subscript T [] = T
    36.7 -  | subscript T _ = raise Subscript;
    36.8 +  | subscript _ _ = raise Subscript;
    36.9  
   36.10  in
   36.11  
    37.1 --- a/src/Pure/context.ML	Thu Oct 01 09:09:56 2009 +0200
    37.2 +++ b/src/Pure/context.ML	Thu Oct 01 11:33:32 2009 +0200
    37.3 @@ -455,7 +455,7 @@
    37.4  
    37.5  fun init_proof thy = Prf (init_data thy, check_thy thy);
    37.6  
    37.7 -fun transfer_proof thy' (prf as Prf (data, thy_ref)) =
    37.8 +fun transfer_proof thy' (Prf (data, thy_ref)) =
    37.9    let
   37.10      val thy = deref thy_ref;
   37.11      val _ = subthy (thy, thy') orelse error "transfer proof context: not a super theory";
    38.1 --- a/src/Pure/defs.ML	Thu Oct 01 09:09:56 2009 +0200
    38.2 +++ b/src/Pure/defs.ML	Thu Oct 01 11:33:32 2009 +0200
    38.3 @@ -123,7 +123,7 @@
    38.4  fun contained (U as TVar _) (Type (_, Ts)) = exists (fn T => T = U orelse contained U T) Ts
    38.5    | contained _ _ = false;
    38.6  
    38.7 -fun acyclic pp defs (c, args) (d, Us) =
    38.8 +fun acyclic pp (c, args) (d, Us) =
    38.9    c <> d orelse
   38.10    exists (fn U => exists (contained U) args) Us orelse
   38.11    is_none (match_args (args, Us)) orelse
   38.12 @@ -150,7 +150,7 @@
   38.13        if forall (is_none o #1) reds then NONE
   38.14        else SOME (fold_rev
   38.15          (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
   38.16 -    val _ = forall (acyclic pp defs const) (the_default deps deps');
   38.17 +    val _ = forall (acyclic pp const) (the_default deps deps');
   38.18    in deps' end;
   38.19  
   38.20  in
   38.21 @@ -163,8 +163,7 @@
   38.22            (args, perhaps (reduction pp defs (c, args)) deps));
   38.23        in
   38.24          if reducts = reducts' then (changed, defs)
   38.25 -        else (true, defs |> map_def c (fn (specs, restricts, reducts) =>
   38.26 -          (specs, restricts, reducts')))
   38.27 +        else (true, defs |> map_def c (fn (specs, restricts, _) => (specs, restricts, reducts')))
   38.28        end;
   38.29      fun norm_all defs =
   38.30        (case Symtab.fold norm_update defs (false, defs) of
   38.31 @@ -206,7 +205,7 @@
   38.32    let
   38.33      val restr =
   38.34        if plain_args args orelse
   38.35 -        (case args of [Type (a, rec_args)] => plain_args rec_args | _ => false)
   38.36 +        (case args of [Type (_, rec_args)] => plain_args rec_args | _ => false)
   38.37        then [] else [(args, name)];
   38.38      val spec =
   38.39        (serial (), {is_def = is_def, name = name, lhs = args, rhs = deps});
    39.1 --- a/src/Pure/display.ML	Thu Oct 01 09:09:56 2009 +0200
    39.2 +++ b/src/Pure/display.ML	Thu Oct 01 11:33:32 2009 +0200
    39.3 @@ -177,7 +177,7 @@
    39.4      val axioms = (Theory.axiom_space thy, Theory.axiom_table thy);
    39.5      val defs = Theory.defs_of thy;
    39.6      val {restricts, reducts} = Defs.dest defs;
    39.7 -    val {naming, syn = _, tsig, consts} = Sign.rep_sg thy;
    39.8 +    val {naming = _, syn = _, tsig, consts} = Sign.rep_sg thy;
    39.9      val {constants, constraints} = Consts.dest consts;
   39.10      val extern_const = NameSpace.extern (#1 constants);
   39.11      val {classes, default, types, ...} = Type.rep_tsig tsig;
    40.1 --- a/src/Pure/envir.ML	Thu Oct 01 09:09:56 2009 +0200
    40.2 +++ b/src/Pure/envir.ML	Thu Oct 01 11:33:32 2009 +0200
    40.3 @@ -62,8 +62,8 @@
    40.4    tenv: tenv,           (*assignments to Vars*)
    40.5    tyenv: Type.tyenv};   (*assignments to TVars*)
    40.6  
    40.7 -fun make_env (maxidx, tenv, tyenv) = Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv};
    40.8 -fun map_env f (Envir {maxidx, tenv, tyenv}) = make_env (f (maxidx, tenv, tyenv));
    40.9 +fun make_env (maxidx, tenv, tyenv) =
   40.10 +  Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv};
   40.11  
   40.12  fun maxidx_of (Envir {maxidx, ...}) = maxidx;
   40.13  fun term_env (Envir {tenv, ...}) = tenv;
    41.1 --- a/src/Pure/goal.ML	Thu Oct 01 09:09:56 2009 +0200
    41.2 +++ b/src/Pure/goal.ML	Thu Oct 01 11:33:32 2009 +0200
    41.3 @@ -300,22 +300,22 @@
    41.4    | SOME st' => Seq.single st');
    41.5  
    41.6  (*parallel refinement of non-schematic goal by single results*)
    41.7 +exception FAILED of unit;
    41.8  fun PARALLEL_GOALS tac st =
    41.9    let
   41.10      val st0 = Thm.adjust_maxidx_thm ~1 st;
   41.11      val _ = Thm.maxidx_of st0 >= 0 andalso
   41.12        raise THM ("PARALLEL_GOALS: schematic goal state", 0, [st]);
   41.13  
   41.14 -    exception FAILED;
   41.15      fun try_tac g =
   41.16        (case SINGLE tac g of
   41.17 -        NONE => raise FAILED
   41.18 +        NONE => raise FAILED ()
   41.19        | SOME g' => g');
   41.20  
   41.21      val goals = Drule.strip_imp_prems (Thm.cprop_of st0);
   41.22      val results = Par_List.map (try_tac o init) goals;
   41.23    in ALLGOALS (fn i => retrofit i 1 (nth results (i - 1))) st0 end
   41.24 -  handle FAILED => Seq.empty;
   41.25 +  handle FAILED () => Seq.empty;
   41.26  
   41.27  end;
   41.28  
    42.1 --- a/src/Pure/logic.ML	Thu Oct 01 09:09:56 2009 +0200
    42.2 +++ b/src/Pure/logic.ML	Thu Oct 01 11:33:32 2009 +0200
    42.3 @@ -222,7 +222,7 @@
    42.4  fun mk_of_class (ty, c) =
    42.5    Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
    42.6  
    42.7 -fun dest_of_class (t as Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
    42.8 +fun dest_of_class (Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
    42.9    | dest_of_class t = raise TERM ("dest_of_class", [t]);
   42.10  
   42.11  
    43.1 --- a/src/Pure/meta_simplifier.ML	Thu Oct 01 09:09:56 2009 +0200
    43.2 +++ b/src/Pure/meta_simplifier.ML	Thu Oct 01 11:33:32 2009 +0200
    43.3 @@ -229,11 +229,6 @@
    43.4  
    43.5  fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2);
    43.6  
    43.7 -fun map_simpset f (Simpset ({rules, prems, bounds, depth, context},
    43.8 -    {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers})) =
    43.9 -  make_simpset (f ((rules, prems, bounds, depth, context),
   43.10 -    (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)));
   43.11 -
   43.12  fun map_simpset1 f (Simpset (r1, r2)) = Simpset (map_ss1 f r1, r2);
   43.13  fun map_simpset2 f (Simpset (r1, r2)) = Simpset (r1, map_ss2 f r2);
   43.14  
   43.15 @@ -388,7 +383,7 @@
   43.16      (Net.delete_term eq_rrule (term_of elhs, rrule) rules, prems, bounds, depth, context))
   43.17    handle Net.DELETE => (cond_warn_thm "Rewrite rule not in simpset:" ss thm; ss);
   43.18  
   43.19 -fun insert_rrule (rrule as {thm, name, elhs, ...}) ss =
   43.20 +fun insert_rrule (rrule as {thm, name, ...}) ss =
   43.21   (trace_named_thm (fn () => "Adding rewrite rule") ss (thm, name);
   43.22    ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) =>
   43.23      let
   43.24 @@ -455,7 +450,6 @@
   43.25    | SOME eq_True =>
   43.26        let
   43.27          val (_, _, lhs, elhs, _, _) = decomp_simp eq_True;
   43.28 -        val extra = rrule_extra_vars elhs eq_True;
   43.29        in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end);
   43.30  
   43.31  (*create the rewrite rule and possibly also the eq_True variant,
   43.32 @@ -869,7 +863,7 @@
   43.33    Otherwise those vars may become instantiated with unnormalized terms
   43.34    while the premises are solved.*)
   43.35  
   43.36 -fun cond_skel (args as (congs, (lhs, rhs))) =
   43.37 +fun cond_skel (args as (_, (lhs, rhs))) =
   43.38    if Term.add_vars rhs [] subset Term.add_vars lhs [] then uncond_skel args
   43.39    else skel0;
   43.40  
   43.41 @@ -892,8 +886,7 @@
   43.42      val eta_t = term_of eta_t';
   43.43      fun rew {thm, name, lhs, elhs, extra, fo, perm} =
   43.44        let
   43.45 -        val thy = Thm.theory_of_thm thm;
   43.46 -        val {prop, maxidx, ...} = rep_thm thm;
   43.47 +        val prop = Thm.prop_of thm;
   43.48          val (rthm, elhs') =
   43.49            if maxt = ~1 orelse not extra then (thm, elhs)
   43.50            else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs);
   43.51 @@ -979,7 +972,7 @@
   43.52        (* Thm.match can raise Pattern.MATCH;
   43.53           is handled when congc is called *)
   43.54        val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
   43.55 -      val unit = trace_thm (fn () => "Applying congruence rule:") ss thm';
   43.56 +      val _ = trace_thm (fn () => "Applying congruence rule:") ss thm';
   43.57        fun err (msg, thm) = (trace_thm (fn () => msg) ss thm; NONE)
   43.58    in case prover thm' of
   43.59         NONE => err ("Congruence proof failed.  Could not prove", thm')
   43.60 @@ -1025,7 +1018,7 @@
   43.61  
   43.62      and subc skel (ss as Simpset ({bounds, ...}, {congs, ...})) t0 =
   43.63         (case term_of t0 of
   43.64 -           Abs (a, T, t) =>
   43.65 +           Abs (a, T, _) =>
   43.66               let
   43.67                   val b = Name.bound (#1 bounds);
   43.68                   val (v, t') = Thm.dest_abs (SOME b) t0;
   43.69 @@ -1124,7 +1117,7 @@
   43.70        end
   43.71  
   43.72      and rebuild [] _ _ _ _ eq = eq
   43.73 -      | rebuild (prem :: prems) concl (rrs :: rrss) (asm :: asms) ss eq =
   43.74 +      | rebuild (prem :: prems) concl (_ :: rrss) (_ :: asms) ss eq =
   43.75            let
   43.76              val ss' = add_rrules (rev rrss, rev asms) ss;
   43.77              val concl' =
   43.78 @@ -1231,7 +1224,7 @@
   43.79    let
   43.80      val thy = Thm.theory_of_cterm raw_ct;
   43.81      val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
   43.82 -    val {t, maxidx, ...} = Thm.rep_cterm ct;
   43.83 +    val {maxidx, ...} = Thm.rep_cterm ct;
   43.84      val ss = inc_simp_depth (activate_context thy raw_ss);
   43.85      val depth = simp_depth ss;
   43.86      val _ =
   43.87 @@ -1297,8 +1290,8 @@
   43.88  (* for folding definitions, handling critical pairs *)
   43.89  
   43.90  (*The depth of nesting in a term*)
   43.91 -fun term_depth (Abs(a,T,t)) = 1 + term_depth t
   43.92 -  | term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t)
   43.93 +fun term_depth (Abs (_, _, t)) = 1 + term_depth t
   43.94 +  | term_depth (f $ t) = 1 + Int.max (term_depth f, term_depth t)
   43.95    | term_depth _ = 0;
   43.96  
   43.97  val lhs_of_thm = #1 o Logic.dest_equals o prop_of;
    44.1 --- a/src/Pure/proofterm.ML	Thu Oct 01 09:09:56 2009 +0200
    44.2 +++ b/src/Pure/proofterm.ML	Thu Oct 01 11:33:32 2009 +0200
    44.3 @@ -959,7 +959,7 @@
    44.4    if ! proofs = 0 then ((name, dummy), Oracle (name, dummy, NONE))
    44.5    else ((name, prop), gen_axm_proof Oracle name prop);
    44.6  
    44.7 -fun shrink_proof thy =
    44.8 +val shrink_proof =
    44.9    let
   44.10      fun shrink ls lev (prf as Abst (a, T, body)) =
   44.11            let val (b, is, ch, body') = shrink ls (lev+1) body
   44.12 @@ -1319,7 +1319,7 @@
   44.13  
   44.14      val proof0 =
   44.15        if ! proofs = 2 then
   44.16 -        #4 (shrink_proof thy [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)))
   44.17 +        #4 (shrink_proof [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)))
   44.18        else MinProof;
   44.19      val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
   44.20  
    45.1 --- a/src/Pure/pure_thy.ML	Thu Oct 01 09:09:56 2009 +0200
    45.2 +++ b/src/Pure/pure_thy.ML	Thu Oct 01 11:33:32 2009 +0200
    45.3 @@ -239,7 +239,6 @@
    45.4  (*** Pure theory syntax and logical content ***)
    45.5  
    45.6  val typ = SimpleSyntax.read_typ;
    45.7 -val term = SimpleSyntax.read_term;
    45.8  val prop = SimpleSyntax.read_prop;
    45.9  
   45.10  val typeT = Syntax.typeT;
    46.1 --- a/src/Pure/sign.ML	Thu Oct 01 09:09:56 2009 +0200
    46.2 +++ b/src/Pure/sign.ML	Thu Oct 01 11:33:32 2009 +0200
    46.3 @@ -68,7 +68,6 @@
    46.4    val certify_typ_mode: Type.mode -> theory -> typ -> typ
    46.5    val certify': bool -> Pretty.pp -> bool -> Consts.T -> theory -> term -> term * typ * int
    46.6    val certify_term: theory -> term -> term * typ * int
    46.7 -  val certify_prop: theory -> term -> term * typ * int
    46.8    val cert_term: theory -> term -> term
    46.9    val cert_prop: theory -> term -> term
   46.10    val no_frees: Pretty.pp -> term -> term
   46.11 @@ -369,11 +368,9 @@
   46.12    in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
   46.13  
   46.14  fun certify_term thy = certify' false (Syntax.pp_global thy) true (consts_of thy) thy;
   46.15 -fun certify_prop thy = certify' true (Syntax.pp_global thy) true (consts_of thy) thy;
   46.16 -
   46.17  fun cert_term_abbrev thy = #1 o certify' false (Syntax.pp_global thy) false (consts_of thy) thy;
   46.18  val cert_term = #1 oo certify_term;
   46.19 -val cert_prop = #1 oo certify_prop;
   46.20 +fun cert_prop thy = #1 o certify' true (Syntax.pp_global thy) true (consts_of thy) thy;
   46.21  
   46.22  end;
   46.23  
    47.1 --- a/src/Pure/simplifier.ML	Thu Oct 01 09:09:56 2009 +0200
    47.2 +++ b/src/Pure/simplifier.ML	Thu Oct 01 11:33:32 2009 +0200
    47.3 @@ -287,8 +287,6 @@
    47.4  
    47.5  val simpN = "simp";
    47.6  val congN = "cong";
    47.7 -val addN = "add";
    47.8 -val delN = "del";
    47.9  val onlyN = "only";
   47.10  val no_asmN = "no_asm";
   47.11  val no_asm_useN = "no_asm_use";
    48.1 --- a/src/Pure/sorts.ML	Thu Oct 01 09:09:56 2009 +0200
    48.2 +++ b/src/Pure/sorts.ML	Thu Oct 01 11:33:32 2009 +0200
    48.3 @@ -57,7 +57,7 @@
    48.4    val meet_sort_typ: algebra -> typ * sort -> typ -> typ   (*exception CLASS_ERROR*)
    48.5    val of_sort: algebra -> typ * sort -> bool
    48.6    val weaken: algebra -> ('a * class -> class -> 'a) -> 'a * class -> class -> 'a
    48.7 -  val of_sort_derivation: Pretty.pp -> algebra ->
    48.8 +  val of_sort_derivation: algebra ->
    48.9      {class_relation: 'a * class -> class -> 'a,
   48.10       type_constructor: string -> ('a * class) list list -> class -> 'a,
   48.11       type_variable: typ -> ('a * class) list} ->
   48.12 @@ -401,7 +401,7 @@
   48.13      | cs :: _ => path (x, cs))
   48.14    end;
   48.15  
   48.16 -fun of_sort_derivation pp algebra {class_relation, type_constructor, type_variable} =
   48.17 +fun of_sort_derivation algebra {class_relation, type_constructor, type_variable} =
   48.18    let
   48.19      val weaken = weaken algebra class_relation;
   48.20      val arities = arities_of algebra;
    49.1 --- a/src/Pure/term.ML	Thu Oct 01 09:09:56 2009 +0200
    49.2 +++ b/src/Pure/term.ML	Thu Oct 01 11:33:32 2009 +0200
    49.3 @@ -796,7 +796,7 @@
    49.4        let
    49.5          fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T)
    49.6            | subst (Free (a, T)) = Free (a, typ_subst_TVars instT T)
    49.7 -          | subst (t as Var (xi, T)) =
    49.8 +          | subst (Var (xi, T)) =
    49.9                (case AList.lookup (op =) inst xi of
   49.10                  NONE => Var (xi, typ_subst_TVars instT T)
   49.11                | SOME t => t)
    50.1 --- a/src/Pure/theory.ML	Thu Oct 01 09:09:56 2009 +0200
    50.2 +++ b/src/Pure/theory.ML	Thu Oct 01 11:33:32 2009 +0200
    50.3 @@ -94,7 +94,8 @@
    50.4    val empty = make_thy (NameSpace.empty_table, Defs.empty, ([], []));
    50.5    val copy = I;
    50.6  
    50.7 -  fun extend (Thy {axioms, defs, wrappers}) = make_thy (NameSpace.empty_table, defs, wrappers);
    50.8 +  fun extend (Thy {axioms = _, defs, wrappers}) =
    50.9 +    make_thy (NameSpace.empty_table, defs, wrappers);
   50.10  
   50.11    fun merge pp (thy1, thy2) =
   50.12      let
   50.13 @@ -155,7 +156,7 @@
   50.14  
   50.15  fun cert_axm thy (b, raw_tm) =
   50.16    let
   50.17 -    val (t, T, _) = Sign.certify_prop thy raw_tm
   50.18 +    val t = Sign.cert_prop thy raw_tm
   50.19        handle TYPE (msg, _, _) => error msg
   50.20          | TERM (msg, _) => error msg;
   50.21    in
    51.1 --- a/src/Pure/thm.ML	Thu Oct 01 09:09:56 2009 +0200
    51.2 +++ b/src/Pure/thm.ML	Thu Oct 01 11:33:32 2009 +0200
    51.3 @@ -181,7 +181,7 @@
    51.4      val sorts = Sorts.insert_typ T [];
    51.5    in Ctyp {thy_ref = Theory.check_thy thy, T = T, maxidx = maxidx, sorts = sorts} end;
    51.6  
    51.7 -fun dest_ctyp (Ctyp {thy_ref, T = Type (s, Ts), maxidx, sorts}) =
    51.8 +fun dest_ctyp (Ctyp {thy_ref, T = Type (_, Ts), maxidx, sorts}) =
    51.9        map (fn T => Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}) Ts
   51.10    | dest_ctyp cT = raise TYPE ("dest_ctyp", [typ_of cT], []);
   51.11  
   51.12 @@ -218,31 +218,31 @@
   51.13      val sorts = Sorts.insert_term t [];
   51.14    in Cterm {thy_ref = Theory.check_thy thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end;
   51.15  
   51.16 -fun merge_thys0 (Cterm {thy_ref = r1, t = t1, ...}) (Cterm {thy_ref = r2, t = t2, ...}) =
   51.17 +fun merge_thys0 (Cterm {thy_ref = r1, ...}) (Cterm {thy_ref = r2, ...}) =
   51.18    Theory.merge_refs (r1, r2);
   51.19  
   51.20  
   51.21  (* destructors *)
   51.22  
   51.23 -fun dest_comb (ct as Cterm {t = c $ a, T, thy_ref, maxidx, sorts}) =
   51.24 +fun dest_comb (Cterm {t = c $ a, T, thy_ref, maxidx, sorts}) =
   51.25        let val A = Term.argument_type_of c 0 in
   51.26          (Cterm {t = c, T = A --> T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts},
   51.27           Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts})
   51.28        end
   51.29    | dest_comb ct = raise CTERM ("dest_comb", [ct]);
   51.30  
   51.31 -fun dest_fun (ct as Cterm {t = c $ _, T, thy_ref, maxidx, sorts}) =
   51.32 +fun dest_fun (Cterm {t = c $ _, T, thy_ref, maxidx, sorts}) =
   51.33        let val A = Term.argument_type_of c 0
   51.34        in Cterm {t = c, T = A --> T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end
   51.35    | dest_fun ct = raise CTERM ("dest_fun", [ct]);
   51.36  
   51.37 -fun dest_arg (ct as Cterm {t = c $ a, T = _, thy_ref, maxidx, sorts}) =
   51.38 +fun dest_arg (Cterm {t = c $ a, T = _, thy_ref, maxidx, sorts}) =
   51.39        let val A = Term.argument_type_of c 0
   51.40        in Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end
   51.41    | dest_arg ct = raise CTERM ("dest_arg", [ct]);
   51.42  
   51.43  
   51.44 -fun dest_fun2 (Cterm {t = c $ a $ b, T, thy_ref, maxidx, sorts}) =
   51.45 +fun dest_fun2 (Cterm {t = c $ _ $ _, T, thy_ref, maxidx, sorts}) =
   51.46        let
   51.47          val A = Term.argument_type_of c 0;
   51.48          val B = Term.argument_type_of c 1;
   51.49 @@ -254,8 +254,7 @@
   51.50        in Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end
   51.51    | dest_arg1 ct = raise CTERM ("dest_arg1", [ct]);
   51.52  
   51.53 -fun dest_abs a (ct as
   51.54 -        Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), thy_ref, maxidx, sorts}) =
   51.55 +fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), thy_ref, maxidx, sorts}) =
   51.56        let val (y', t') = Term.dest_abs (the_default x a, T, t) in
   51.57          (Cterm {t = Free (y', T), T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts},
   51.58            Cterm {t = t', T = U, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts})
   51.59 @@ -392,10 +391,10 @@
   51.60  
   51.61  (* merge theories of cterms/thms -- trivial absorption only *)
   51.62  
   51.63 -fun merge_thys1 (Cterm {thy_ref = r1, ...}) (th as Thm (_, {thy_ref = r2, ...})) =
   51.64 +fun merge_thys1 (Cterm {thy_ref = r1, ...}) (Thm (_, {thy_ref = r2, ...})) =
   51.65    Theory.merge_refs (r1, r2);
   51.66  
   51.67 -fun merge_thys2 (th1 as Thm (_, {thy_ref = r1, ...})) (th2 as Thm (_, {thy_ref = r2, ...})) =
   51.68 +fun merge_thys2 (Thm (_, {thy_ref = r1, ...})) (Thm (_, {thy_ref = r2, ...})) =
   51.69    Theory.merge_refs (r1, r2);
   51.70  
   51.71  
   51.72 @@ -808,7 +807,7 @@
   51.73  (*Reflexivity
   51.74    t == t
   51.75  *)
   51.76 -fun reflexive (ct as Cterm {thy_ref, t, T, maxidx, sorts}) =
   51.77 +fun reflexive (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
   51.78    Thm (deriv_rule0 Pt.reflexive,
   51.79     {thy_ref = thy_ref,
   51.80      tags = [],
   51.81 @@ -825,7 +824,7 @@
   51.82  *)
   51.83  fun symmetric (th as Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
   51.84    (case prop of
   51.85 -    (eq as Const ("==", Type (_, [T, _]))) $ t $ u =>
   51.86 +    (eq as Const ("==", _)) $ t $ u =>
   51.87        Thm (deriv_rule1 Pt.symmetric der,
   51.88         {thy_ref = thy_ref,
   51.89          tags = [],
   51.90 @@ -868,7 +867,7 @@
   51.91    (%x. t)(u) == t[u/x]
   51.92    fully beta-reduces the term if full = true
   51.93  *)
   51.94 -fun beta_conversion full (Cterm {thy_ref, t, T, maxidx, sorts}) =
   51.95 +fun beta_conversion full (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
   51.96    let val t' =
   51.97      if full then Envir.beta_norm t
   51.98      else
   51.99 @@ -885,7 +884,7 @@
  51.100        prop = Logic.mk_equals (t, t')})
  51.101    end;
  51.102  
  51.103 -fun eta_conversion (Cterm {thy_ref, t, T, maxidx, sorts}) =
  51.104 +fun eta_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
  51.105    Thm (deriv_rule0 Pt.reflexive,
  51.106     {thy_ref = thy_ref,
  51.107      tags = [],
  51.108 @@ -895,7 +894,7 @@
  51.109      tpairs = [],
  51.110      prop = Logic.mk_equals (t, Envir.eta_contract t)});
  51.111  
  51.112 -fun eta_long_conversion (Cterm {thy_ref, t, T, maxidx, sorts}) =
  51.113 +fun eta_long_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
  51.114    Thm (deriv_rule0 Pt.reflexive,
  51.115     {thy_ref = thy_ref,
  51.116      tags = [],
  51.117 @@ -951,7 +950,7 @@
  51.118        prop = prop2, ...}) = th2;
  51.119      fun chktypes fT tT =
  51.120        (case fT of
  51.121 -        Type ("fun", [T1, T2]) =>
  51.122 +        Type ("fun", [T1, _]) =>
  51.123            if T1 <> tT then
  51.124              raise THM ("combination: types", 0, [th1, th2])
  51.125            else ()
  51.126 @@ -1264,7 +1263,7 @@
  51.127  val varifyT = #2 o varifyT' [];
  51.128  
  51.129  (* Replace all TVars by new TFrees *)
  51.130 -fun freezeT (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
  51.131 +fun freezeT (Thm (der, {thy_ref, shyps, hyps, tpairs, prop, ...})) =
  51.132    let
  51.133      val prop1 = attach_tpairs tpairs prop;
  51.134      val prop2 = Type.freeze prop1;
  51.135 @@ -1329,7 +1328,7 @@
  51.136  (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
  51.137  fun assumption i state =
  51.138    let
  51.139 -    val Thm (der, {thy_ref, maxidx, shyps, hyps, prop, ...}) = state;
  51.140 +    val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state;
  51.141      val thy = Theory.deref thy_ref;
  51.142      val (tpairs, Bs, Bi, C) = dest_state (state, i);
  51.143      fun newth n (env, tpairs) =
  51.144 @@ -1365,7 +1364,7 @@
  51.145    Checks if Bi's conclusion is alpha-convertible to one of its assumptions*)
  51.146  fun eq_assumption i state =
  51.147    let
  51.148 -    val Thm (der, {thy_ref, maxidx, shyps, hyps, prop, ...}) = state;
  51.149 +    val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state;
  51.150      val (tpairs, Bs, Bi, C) = dest_state (state, i);
  51.151      val (_, asms, concl) = Logic.assum_problems (~1, Bi);
  51.152    in
  51.153 @@ -1386,7 +1385,7 @@
  51.154  (*For rotate_tac: fast rotation of assumptions of subgoal i*)
  51.155  fun rotate_rule k i state =
  51.156    let
  51.157 -    val Thm (der, {thy_ref, maxidx, shyps, hyps, prop, ...}) = state;
  51.158 +    val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state;
  51.159      val (tpairs, Bs, Bi, C) = dest_state (state, i);
  51.160      val params = Term.strip_all_vars Bi
  51.161      and rest   = Term.strip_all_body Bi;
  51.162 @@ -1558,7 +1557,7 @@
  51.163        in Term.all T' $ Abs (a, T', norm_term_skip env n t) end
  51.164    | norm_term_skip env n (Const ("==>", _) $ A $ B) =
  51.165        Logic.mk_implies (A, norm_term_skip env (n - 1) B)
  51.166 -  | norm_term_skip env n t = error "norm_term_skip: too few assumptions??";
  51.167 +  | norm_term_skip _ _ _ = error "norm_term_skip: too few assumptions??";
  51.168  
  51.169  
  51.170  (*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C)
    52.1 --- a/src/Pure/type.ML	Thu Oct 01 09:09:56 2009 +0200
    52.2 +++ b/src/Pure/type.ML	Thu Oct 01 11:33:32 2009 +0200
    52.3 @@ -140,7 +140,7 @@
    52.4  fun cert_class (TSig {classes, ...}) = Sorts.certify_class (#2 classes);
    52.5  fun cert_sort (TSig {classes, ...}) = Sorts.certify_sort (#2 classes);
    52.6  
    52.7 -fun witness_sorts (tsig as TSig {classes, log_types, ...}) =
    52.8 +fun witness_sorts (TSig {classes, log_types, ...}) =
    52.9    Sorts.witness_sorts (#2 classes) log_types;
   52.10  
   52.11  
   52.12 @@ -280,7 +280,7 @@
   52.13      val used = Name.context
   52.14        |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
   52.15      val fmap = fs ~~ map (rpair 0) (#1 (Name.variants (map fst fs) used));
   52.16 -    fun thaw (f as (a, S)) =
   52.17 +    fun thaw (f as (_, S)) =
   52.18        (case AList.lookup (op =) fmap f of
   52.19          NONE => TFree f
   52.20        | SOME xi => TVar (xi, S));
   52.21 @@ -412,10 +412,10 @@
   52.22        (case lookup tye v of
   52.23          SOME U => devar tye U
   52.24        | NONE => T)
   52.25 -  | devar tye T = T;
   52.26 +  | devar _ T = T;
   52.27  
   52.28  (*order-sorted unification*)
   52.29 -fun unify (tsig as TSig {classes = (_, classes), ...}) TU (tyenv, maxidx) =
   52.30 +fun unify (TSig {classes = (_, classes), ...}) TU (tyenv, maxidx) =
   52.31    let
   52.32      val tyvar_count = Unsynchronized.ref maxidx;
   52.33      fun gen_tyvar S = TVar ((Name.aT, Unsynchronized.inc tyvar_count), S);
   52.34 @@ -465,7 +465,7 @@
   52.35  (*purely structural unification*)
   52.36  fun raw_unify (ty1, ty2) tye =
   52.37    (case (devar tye ty1, devar tye ty2) of
   52.38 -    (T as TVar (v, S1), U as TVar (w, S2)) =>
   52.39 +    (T as TVar (v, S1), TVar (w, S2)) =>
   52.40        if Term.eq_ix (v, w) then
   52.41          if S1 = S2 then tye else tvar_clash v S1 S2
   52.42        else Vartab.update_new (w, (S2, T)) tye
   52.43 @@ -545,7 +545,7 @@
   52.44      let
   52.45        val rel' = pairself (cert_class tsig) rel
   52.46          handle TYPE (msg, _, _) => error msg;
   52.47 -      val classes' = classes |> Sorts.add_classrel pp rel;
   52.48 +      val classes' = classes |> Sorts.add_classrel pp rel';
   52.49      in ((space, classes'), default, types) end);
   52.50  
   52.51  
    53.1 --- a/src/Pure/variable.ML	Thu Oct 01 09:09:56 2009 +0200
    53.2 +++ b/src/Pure/variable.ML	Thu Oct 01 11:33:32 2009 +0200
    53.3 @@ -89,7 +89,7 @@
    53.4  structure Data = ProofDataFun
    53.5  (
    53.6    type T = data;
    53.7 -  fun init thy =
    53.8 +  fun init _ =
    53.9      make_data (false, Name.context, Symtab.empty, [], Vartab.empty, Symtab.empty,
   53.10        ~1, [], (Vartab.empty, Vartab.empty));
   53.11  );
    54.1 --- a/src/Tools/Code/code_preproc.ML	Thu Oct 01 09:09:56 2009 +0200
    54.2 +++ b/src/Tools/Code/code_preproc.ML	Thu Oct 01 11:33:32 2009 +0200
    54.3 @@ -403,7 +403,7 @@
    54.4          @ (maps o maps) fst xs;
    54.5      fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
    54.6    in
    54.7 -    flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
    54.8 +    flat (Sorts.of_sort_derivation algebra
    54.9        { class_relation = class_relation, type_constructor = type_constructor,
   54.10          type_variable = type_variable } (T, proj_sort sort)
   54.11         handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
    55.1 --- a/src/Tools/Code/code_thingol.ML	Thu Oct 01 09:09:56 2009 +0200
    55.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Oct 01 11:33:32 2009 +0200
    55.3 @@ -750,7 +750,6 @@
    55.4    #>> (fn sort => (unprefix "'" v, sort))
    55.5  and translate_dicts thy (algbr as (proj_sort, algebra)) funcgr thm (ty, sort) =
    55.6    let
    55.7 -    val pp = Syntax.pp_global thy;
    55.8      datatype typarg =
    55.9          Global of (class * string) * typarg list list
   55.10        | Local of (class * class) list * (string * (int * sort));
   55.11 @@ -764,7 +763,7 @@
   55.12        let
   55.13          val sort' = proj_sort sort;
   55.14        in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
   55.15 -    val typargs = Sorts.of_sort_derivation pp algebra
   55.16 +    val typargs = Sorts.of_sort_derivation algebra
   55.17        {class_relation = class_relation, type_constructor = type_constructor,
   55.18         type_variable = type_variable} (ty, proj_sort sort)
   55.19        handle Sorts.CLASS_ERROR e => not_wellsorted thy thm ty sort e;