# HG changeset patch # User wenzelm # Date 1254342058 -7200 # Node ID 1a5dde5079ac562785fe96b4ae0f22aacfcc9306 # Parent e43d761a742d56ebd9623550fd649b6503887873 eliminated redundant bindings; diff -r e43d761a742d -r 1a5dde5079ac src/Pure/Concurrent/task_queue.ML --- a/src/Pure/Concurrent/task_queue.ML Wed Sep 30 19:04:48 2009 +0200 +++ b/src/Pure/Concurrent/task_queue.ML Wed Sep 30 22:20:58 2009 +0200 @@ -125,7 +125,7 @@ fun status (Queue {jobs, ...}) = let val (x, y, z) = - Task_Graph.fold (fn (task, ((_, job), (deps, _))) => fn (x, y, z) => + Task_Graph.fold (fn (_, ((_, job), (deps, _))) => fn (x, y, z) => (case job of Job _ => if null deps then (x + 1, y, z) else (x, y + 1, z) | Running _ => (x, y, z + 1))) diff -r e43d761a742d -r 1a5dde5079ac src/Pure/General/heap.ML --- a/src/Pure/General/heap.ML Wed Sep 30 19:04:48 2009 +0200 +++ b/src/Pure/General/heap.ML Wed Sep 30 22:20:58 2009 +0200 @@ -78,8 +78,8 @@ nonfix upto; -fun upto _ (h as Empty) = ([], h) - | upto limit (h as Heap (_, x, a, b)) = +fun upto _ Empty = ([], Empty) + | upto limit (h as Heap (_, x, _, _)) = (case ord (x, limit) of GREATER => ([], h) | _ => upto limit (delete_min h) |>> cons x); diff -r e43d761a742d -r 1a5dde5079ac src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Wed Sep 30 19:04:48 2009 +0200 +++ b/src/Pure/General/pretty.ML Wed Sep 30 22:20:58 2009 +0200 @@ -197,11 +197,11 @@ fun setdepth dp = (depth := dp); local - fun pruning dp (Block (m, bes, indent, wd)) = + fun pruning dp (Block (m, bes, indent, _)) = if dp > 0 then block_markup m (indent, map (pruning (dp - 1)) bes) else str "..." - | pruning dp e = e + | pruning _ e = e; in fun prune e = if ! depth > 0 then pruning (! depth) e else e; end; @@ -219,7 +219,7 @@ pos = 0, nl = 0}; -fun newline {tx, ind, pos, nl} : text = +fun newline {tx, ind = _, pos = _, nl} : text = {tx = Buffer.add (Output.output "\n") tx, ind = Buffer.empty, pos = 0, @@ -250,22 +250,22 @@ (*Add the lengths of the expressions until the next Break; if no Break then include "after", to account for text following this block.*) fun breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after) - | breakdist (String (s, len) :: es, after) = len + breakdist (es, after) - | breakdist (Break _ :: es, after) = 0 + | breakdist (String (_, len) :: es, after) = len + breakdist (es, after) + | breakdist (Break _ :: _, _) = 0 | breakdist ([], after) = after; (*Search for the next break (at this or higher levels) and force it to occur.*) fun forcenext [] = [] - | forcenext (Break (_, wd) :: es) = Break (true, 0) :: es + | forcenext (Break _ :: es) = Break (true, 0) :: es | forcenext (e :: es) = e :: forcenext es; (*es is list of expressions to print; blockin is the indentation of the current block; after is the width of the following context until next break.*) fun format ([], _, _) text = text - | format (e :: es, block as (blockind, blockin), after) (text as {ind, pos, nl, ...}) = + | format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) = (case e of - Block ((bg, en), bes, indent, wd) => + Block ((bg, en), bes, indent, _) => let val {emergencypos, ...} = ! margin_info; val pos' = pos + indent; diff -r e43d761a742d -r 1a5dde5079ac src/Pure/General/scan.ML --- a/src/Pure/General/scan.ML Wed Sep 30 19:04:48 2009 +0200 +++ b/src/Pure/General/scan.ML Wed Sep 30 22:20:58 2009 +0200 @@ -273,7 +273,7 @@ val empty_lexicon = Lexicon Symtab.empty; fun is_literal _ [] = false - | is_literal (Lexicon tab) (chs as c :: cs) = + | is_literal (Lexicon tab) (c :: cs) = (case Symtab.lookup tab c of SOME (tip, lex) => tip andalso null cs orelse is_literal lex cs | NONE => false); @@ -286,7 +286,7 @@ fun finish (SOME (res, rest)) = (rev res, rest) | finish NONE = raise FAIL NONE; fun scan _ res (Lexicon tab) [] = if Symtab.is_empty tab then finish res else raise MORE NONE - | scan path res (Lexicon tab) (chs as c :: cs) = + | scan path res (Lexicon tab) (c :: cs) = (case Symtab.lookup tab (fst c) of SOME (tip, lex) => let val path' = c :: path @@ -300,7 +300,7 @@ fun extend_lexicon chrs lexicon = let fun ext [] lex = lex - | ext (chs as c :: cs) (Lexicon tab) = + | ext (c :: cs) (Lexicon tab) = (case Symtab.lookup tab c of SOME (tip, lex) => Lexicon (Symtab.update (c, (tip orelse null cs, ext cs lex)) tab) | NONE => Lexicon (Symtab.update (c, (null cs, ext cs empty_lexicon)) tab)); diff -r e43d761a742d -r 1a5dde5079ac src/Pure/General/symbol_pos.ML --- a/src/Pure/General/symbol_pos.ML Wed Sep 30 19:04:48 2009 +0200 +++ b/src/Pure/General/symbol_pos.ML Wed Sep 30 22:20:58 2009 +0200 @@ -161,7 +161,7 @@ fun pad [] = [] | pad [(s, _)] = [s] - | pad ((s1, pos1) :: (rest as (s2, pos2) :: _)) = + | pad ((s1, pos1) :: (rest as (_, pos2) :: _)) = let val end_pos1 = Position.advance s1 pos1; val d = Int.max (0, Position.distance_of end_pos1 pos2); diff -r e43d761a742d -r 1a5dde5079ac src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Wed Sep 30 19:04:48 2009 +0200 +++ b/src/Pure/Isar/args.ML Wed Sep 30 22:20:58 2009 +0200 @@ -283,7 +283,7 @@ (** syntax wrapper **) -fun syntax kind scan (src as Src ((s, args), pos)) st = +fun syntax kind scan (Src ((s, args), pos)) st = (case Scan.error (Scan.finite' T.stopper (Scan.option scan)) (st, args) of (SOME x, (st', [])) => (x, st') | (_, (_, args')) => diff -r e43d761a742d -r 1a5dde5079ac src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Wed Sep 30 19:04:48 2009 +0200 +++ b/src/Pure/Isar/context_rules.ML Wed Sep 30 22:20:58 2009 +0200 @@ -131,8 +131,8 @@ (* retrieving rules *) fun untaglist [] = [] - | untaglist [(k : int * int, x)] = [x] - | untaglist ((k, x) :: (rest as (k', x') :: _)) = + | untaglist [(_ : int * int, x)] = [x] + | untaglist ((k, x) :: (rest as (k', _) :: _)) = if k = k' then untaglist rest else x :: untaglist rest; @@ -160,7 +160,7 @@ (* wrappers *) fun gen_add_wrapper upd w = - Context.theory_map (Rules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) => + Context.theory_map (Rules.map (fn Rules {next, rules, netpairs, wrappers} => make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers))); val addSWrapper = gen_add_wrapper Library.apfst; diff -r e43d761a742d -r 1a5dde5079ac src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Sep 30 19:04:48 2009 +0200 +++ b/src/Pure/Isar/proof_context.ML Wed Sep 30 22:20:58 2009 +0200 @@ -1033,7 +1033,7 @@ local -fun const_syntax ctxt (Free (x, T), mx) = SOME (true, (x, T, mx)) +fun const_syntax _ (Free (x, T), mx) = SOME (true, (x, T, mx)) | const_syntax ctxt (Const (c, _), mx) = Option.map (pair false) (try (Consts.syntax (consts_of ctxt)) (c, mx)) | const_syntax _ _ = NONE; @@ -1106,7 +1106,7 @@ (* fixes vs. frees *) -fun auto_fixes (arg as (ctxt, (propss, x))) = +fun auto_fixes (ctxt, (propss, x)) = ((fold o fold) Variable.auto_fixes propss ctxt, (propss, x)); fun bind_fixes xs ctxt = diff -r e43d761a742d -r 1a5dde5079ac src/Pure/Isar/proof_node.ML --- a/src/Pure/Isar/proof_node.ML Wed Sep 30 19:04:48 2009 +0200 +++ b/src/Pure/Isar/proof_node.ML Wed Sep 30 22:20:58 2009 +0200 @@ -41,7 +41,7 @@ (* apply transformer *) -fun applys f (ProofNode (node as (st, _), n)) = +fun applys f (ProofNode ((st, _), n)) = (case Seq.pull (f st) of NONE => error "empty result sequence -- proof command failed" | SOME res => ProofNode (res, n + 1)); diff -r e43d761a742d -r 1a5dde5079ac src/Pure/Isar/rule_insts.ML --- a/src/Pure/Isar/rule_insts.ML Wed Sep 30 19:04:48 2009 +0200 +++ b/src/Pure/Isar/rule_insts.ML Wed Sep 30 22:20:58 2009 +0200 @@ -266,8 +266,8 @@ let val thy = ProofContext.theory_of ctxt; (* Separate type and term insts *) - fun has_type_var ((x, _), _) = (case Symbol.explode x of - "'"::cs => true | cs => false); + fun has_type_var ((x, _), _) = + (case Symbol.explode x of "'" :: _ => true | _ => false); val Tinsts = List.filter has_type_var insts; val tinsts = filter_out has_type_var insts; diff -r e43d761a742d -r 1a5dde5079ac src/Pure/ML/ml_antiquote.ML --- a/src/Pure/ML/ml_antiquote.ML Wed Sep 30 19:04:48 2009 +0200 +++ b/src/Pure/ML/ml_antiquote.ML Wed Sep 30 22:20:58 2009 +0200 @@ -41,7 +41,7 @@ (Context.Proof ctxt, fn {background, ...} => (K ("", ""), background))))); fun inline name scan = ML_Context.add_antiq name - (fn _ => scan >> (fn s => fn {struct_name, background} => (K ("", s), background))); + (fn _ => scan >> (fn s => fn {background, ...} => (K ("", s), background))); fun declaration kind name scan = ML_Context.add_antiq name (fn _ => scan >> (fn s => fn {struct_name, background} => diff -r e43d761a742d -r 1a5dde5079ac src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Wed Sep 30 19:04:48 2009 +0200 +++ b/src/Pure/Proof/extraction.ML Wed Sep 30 22:20:58 2009 +0200 @@ -81,8 +81,7 @@ {next = next - 1, rs = r :: rs, net = Net.insert_term (K false) (Envir.eta_contract lhs, (next, r)) net}; -fun merge_rules - ({next, rs = rs1, net} : rules) ({next = next2, rs = rs2, ...} : rules) = +fun merge_rules ({next, rs = rs1, net} : rules) ({rs = rs2, ...} : rules) = List.foldr add_rule {next = next, rs = rs1, net = net} (subtract (op =) rs1 rs2); fun condrew thy rules procs = @@ -141,7 +140,7 @@ map_proof_terms (subst_TVars tye) (typ_subst_TVars tye); fun relevant_vars types prop = List.foldr (fn - (Var ((a, i), T), vs) => (case strip_type T of + (Var ((a, _), T), vs) => (case strip_type T of (_, Type (s, _)) => if member (op =) types s then a :: vs else vs | _ => vs) | (_, vs) => vs) [] (vars_of prop); diff -r e43d761a742d -r 1a5dde5079ac src/Pure/Syntax/ast.ML --- a/src/Pure/Syntax/ast.ML Wed Sep 30 19:04:48 2009 +0200 +++ b/src/Pure/Syntax/ast.ML Wed Sep 30 22:20:58 2009 +0200 @@ -94,7 +94,7 @@ (** check translation rules **) -fun rule_error (rule as (lhs, rhs)) = +fun rule_error (lhs, rhs) = let fun add_vars (Constant _) = I | add_vars (Variable x) = cons x diff -r e43d761a742d -r 1a5dde5079ac src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Wed Sep 30 19:04:48 2009 +0200 +++ b/src/Pure/Syntax/syntax.ML Wed Sep 30 22:20:58 2009 +0200 @@ -404,7 +404,7 @@ fun pretty_gram (Syntax (tabs, _)) = let - val {lexicon, prmodes, gram, prtabs, ...} = tabs; + val {lexicon, prmodes, gram, ...} = tabs; val prmodes' = sort_strings (filter_out (fn s => s = "") prmodes); in [pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon), @@ -639,7 +639,7 @@ local -fun unparse_t t_to_ast prt_t markup ctxt (syn as Syntax (tabs, _)) curried t = +fun unparse_t t_to_ast prt_t markup ctxt (Syntax (tabs, _)) curried t = let val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs; val ast = t_to_ast ctxt (lookup_tr' print_trtab) t; diff -r e43d761a742d -r 1a5dde5079ac src/Pure/Syntax/type_ext.ML --- a/src/Pure/Syntax/type_ext.ML Wed Sep 30 19:04:48 2009 +0200 +++ b/src/Pure/Syntax/type_ext.ML Wed Sep 30 22:20:58 2009 +0200 @@ -82,8 +82,8 @@ if Lexicon.is_tid x then TFree (x, get_sort (x, ~1)) else Type (x, []) | typ_of (Var (xi, _)) = TVar (xi, get_sort xi) - | typ_of (Const ("_tfree",_) $ (t as Free x)) = typ_of t - | typ_of (Const ("_tvar",_) $ (t as Var x)) = typ_of t + | typ_of (Const ("_tfree",_) $ (t as Free _)) = typ_of t + | typ_of (Const ("_tvar",_) $ (t as Var _)) = typ_of t | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1)) | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) = TFree (x, get_sort (x, ~1)) diff -r e43d761a742d -r 1a5dde5079ac src/Pure/consts.ML --- a/src/Pure/consts.ML Wed Sep 30 19:04:48 2009 +0200 +++ b/src/Pure/consts.ML Wed Sep 30 22:20:58 2009 +0200 @@ -199,7 +199,7 @@ fun subscript (Type (_, Ts)) (i :: is) = subscript (nth Ts i) is | subscript T [] = T - | subscript T _ = raise Subscript; + | subscript _ _ = raise Subscript; in diff -r e43d761a742d -r 1a5dde5079ac src/Pure/context.ML --- a/src/Pure/context.ML Wed Sep 30 19:04:48 2009 +0200 +++ b/src/Pure/context.ML Wed Sep 30 22:20:58 2009 +0200 @@ -455,7 +455,7 @@ fun init_proof thy = Prf (init_data thy, check_thy thy); -fun transfer_proof thy' (prf as Prf (data, thy_ref)) = +fun transfer_proof thy' (Prf (data, thy_ref)) = let val thy = deref thy_ref; val _ = subthy (thy, thy') orelse error "transfer proof context: not a super theory"; diff -r e43d761a742d -r 1a5dde5079ac src/Pure/display.ML --- a/src/Pure/display.ML Wed Sep 30 19:04:48 2009 +0200 +++ b/src/Pure/display.ML Wed Sep 30 22:20:58 2009 +0200 @@ -177,7 +177,7 @@ val axioms = (Theory.axiom_space thy, Theory.axiom_table thy); val defs = Theory.defs_of thy; val {restricts, reducts} = Defs.dest defs; - val {naming, syn = _, tsig, consts} = Sign.rep_sg thy; + val {naming = _, syn = _, tsig, consts} = Sign.rep_sg thy; val {constants, constraints} = Consts.dest consts; val extern_const = NameSpace.extern (#1 constants); val {classes, default, types, ...} = Type.rep_tsig tsig; diff -r e43d761a742d -r 1a5dde5079ac src/Pure/logic.ML --- a/src/Pure/logic.ML Wed Sep 30 19:04:48 2009 +0200 +++ b/src/Pure/logic.ML Wed Sep 30 22:20:58 2009 +0200 @@ -222,7 +222,7 @@ fun mk_of_class (ty, c) = Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty; -fun dest_of_class (t as Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class) +fun dest_of_class (Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class) | dest_of_class t = raise TERM ("dest_of_class", [t]); diff -r e43d761a742d -r 1a5dde5079ac src/Pure/term.ML --- a/src/Pure/term.ML Wed Sep 30 19:04:48 2009 +0200 +++ b/src/Pure/term.ML Wed Sep 30 22:20:58 2009 +0200 @@ -796,7 +796,7 @@ let fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T) | subst (Free (a, T)) = Free (a, typ_subst_TVars instT T) - | subst (t as Var (xi, T)) = + | subst (Var (xi, T)) = (case AList.lookup (op =) inst xi of NONE => Var (xi, typ_subst_TVars instT T) | SOME t => t) diff -r e43d761a742d -r 1a5dde5079ac src/Pure/thm.ML --- a/src/Pure/thm.ML Wed Sep 30 19:04:48 2009 +0200 +++ b/src/Pure/thm.ML Wed Sep 30 22:20:58 2009 +0200 @@ -181,7 +181,7 @@ val sorts = Sorts.insert_typ T []; in Ctyp {thy_ref = Theory.check_thy thy, T = T, maxidx = maxidx, sorts = sorts} end; -fun dest_ctyp (Ctyp {thy_ref, T = Type (s, Ts), maxidx, sorts}) = +fun dest_ctyp (Ctyp {thy_ref, T = Type (_, Ts), maxidx, sorts}) = map (fn T => Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}) Ts | dest_ctyp cT = raise TYPE ("dest_ctyp", [typ_of cT], []); @@ -218,31 +218,31 @@ val sorts = Sorts.insert_term t []; in Cterm {thy_ref = Theory.check_thy thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end; -fun merge_thys0 (Cterm {thy_ref = r1, t = t1, ...}) (Cterm {thy_ref = r2, t = t2, ...}) = +fun merge_thys0 (Cterm {thy_ref = r1, ...}) (Cterm {thy_ref = r2, ...}) = Theory.merge_refs (r1, r2); (* destructors *) -fun dest_comb (ct as Cterm {t = c $ a, T, thy_ref, maxidx, sorts}) = +fun dest_comb (Cterm {t = c $ a, T, thy_ref, maxidx, sorts}) = let val A = Term.argument_type_of c 0 in (Cterm {t = c, T = A --> T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}, Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}) end | dest_comb ct = raise CTERM ("dest_comb", [ct]); -fun dest_fun (ct as Cterm {t = c $ _, T, thy_ref, maxidx, sorts}) = +fun dest_fun (Cterm {t = c $ _, T, thy_ref, maxidx, sorts}) = let val A = Term.argument_type_of c 0 in Cterm {t = c, T = A --> T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end | dest_fun ct = raise CTERM ("dest_fun", [ct]); -fun dest_arg (ct as Cterm {t = c $ a, T = _, thy_ref, maxidx, sorts}) = +fun dest_arg (Cterm {t = c $ a, T = _, thy_ref, maxidx, sorts}) = let val A = Term.argument_type_of c 0 in Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end | dest_arg ct = raise CTERM ("dest_arg", [ct]); -fun dest_fun2 (Cterm {t = c $ a $ b, T, thy_ref, maxidx, sorts}) = +fun dest_fun2 (Cterm {t = c $ _ $ _, T, thy_ref, maxidx, sorts}) = let val A = Term.argument_type_of c 0; val B = Term.argument_type_of c 1; @@ -254,8 +254,7 @@ in Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end | dest_arg1 ct = raise CTERM ("dest_arg1", [ct]); -fun dest_abs a (ct as - Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), thy_ref, maxidx, sorts}) = +fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), thy_ref, maxidx, sorts}) = let val (y', t') = Term.dest_abs (the_default x a, T, t) in (Cterm {t = Free (y', T), T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}, Cterm {t = t', T = U, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}) @@ -392,10 +391,10 @@ (* merge theories of cterms/thms -- trivial absorption only *) -fun merge_thys1 (Cterm {thy_ref = r1, ...}) (th as Thm (_, {thy_ref = r2, ...})) = +fun merge_thys1 (Cterm {thy_ref = r1, ...}) (Thm (_, {thy_ref = r2, ...})) = Theory.merge_refs (r1, r2); -fun merge_thys2 (th1 as Thm (_, {thy_ref = r1, ...})) (th2 as Thm (_, {thy_ref = r2, ...})) = +fun merge_thys2 (Thm (_, {thy_ref = r1, ...})) (Thm (_, {thy_ref = r2, ...})) = Theory.merge_refs (r1, r2); @@ -808,7 +807,7 @@ (*Reflexivity t == t *) -fun reflexive (ct as Cterm {thy_ref, t, T, maxidx, sorts}) = +fun reflexive (Cterm {thy_ref, t, T = _, maxidx, sorts}) = Thm (deriv_rule0 Pt.reflexive, {thy_ref = thy_ref, tags = [], @@ -825,7 +824,7 @@ *) fun symmetric (th as Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) = (case prop of - (eq as Const ("==", Type (_, [T, _]))) $ t $ u => + (eq as Const ("==", _)) $ t $ u => Thm (deriv_rule1 Pt.symmetric der, {thy_ref = thy_ref, tags = [], @@ -868,7 +867,7 @@ (%x. t)(u) == t[u/x] fully beta-reduces the term if full = true *) -fun beta_conversion full (Cterm {thy_ref, t, T, maxidx, sorts}) = +fun beta_conversion full (Cterm {thy_ref, t, T = _, maxidx, sorts}) = let val t' = if full then Envir.beta_norm t else @@ -885,7 +884,7 @@ prop = Logic.mk_equals (t, t')}) end; -fun eta_conversion (Cterm {thy_ref, t, T, maxidx, sorts}) = +fun eta_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) = Thm (deriv_rule0 Pt.reflexive, {thy_ref = thy_ref, tags = [], @@ -895,7 +894,7 @@ tpairs = [], prop = Logic.mk_equals (t, Envir.eta_contract t)}); -fun eta_long_conversion (Cterm {thy_ref, t, T, maxidx, sorts}) = +fun eta_long_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) = Thm (deriv_rule0 Pt.reflexive, {thy_ref = thy_ref, tags = [], @@ -951,7 +950,7 @@ prop = prop2, ...}) = th2; fun chktypes fT tT = (case fT of - Type ("fun", [T1, T2]) => + Type ("fun", [T1, _]) => if T1 <> tT then raise THM ("combination: types", 0, [th1, th2]) else () @@ -1264,7 +1263,7 @@ val varifyT = #2 o varifyT' []; (* Replace all TVars by new TFrees *) -fun freezeT (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) = +fun freezeT (Thm (der, {thy_ref, shyps, hyps, tpairs, prop, ...})) = let val prop1 = attach_tpairs tpairs prop; val prop2 = Type.freeze prop1; @@ -1329,7 +1328,7 @@ (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *) fun assumption i state = let - val Thm (der, {thy_ref, maxidx, shyps, hyps, prop, ...}) = state; + val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state; val thy = Theory.deref thy_ref; val (tpairs, Bs, Bi, C) = dest_state (state, i); fun newth n (env, tpairs) = @@ -1365,7 +1364,7 @@ Checks if Bi's conclusion is alpha-convertible to one of its assumptions*) fun eq_assumption i state = let - val Thm (der, {thy_ref, maxidx, shyps, hyps, prop, ...}) = state; + val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state; val (tpairs, Bs, Bi, C) = dest_state (state, i); val (_, asms, concl) = Logic.assum_problems (~1, Bi); in @@ -1386,7 +1385,7 @@ (*For rotate_tac: fast rotation of assumptions of subgoal i*) fun rotate_rule k i state = let - val Thm (der, {thy_ref, maxidx, shyps, hyps, prop, ...}) = state; + val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state; val (tpairs, Bs, Bi, C) = dest_state (state, i); val params = Term.strip_all_vars Bi and rest = Term.strip_all_body Bi; @@ -1558,7 +1557,7 @@ in Term.all T' $ Abs (a, T', norm_term_skip env n t) end | norm_term_skip env n (Const ("==>", _) $ A $ B) = Logic.mk_implies (A, norm_term_skip env (n - 1) B) - | norm_term_skip env n t = error "norm_term_skip: too few assumptions??"; + | norm_term_skip _ _ _ = error "norm_term_skip: too few assumptions??"; (*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C) diff -r e43d761a742d -r 1a5dde5079ac src/Pure/type.ML --- a/src/Pure/type.ML Wed Sep 30 19:04:48 2009 +0200 +++ b/src/Pure/type.ML Wed Sep 30 22:20:58 2009 +0200 @@ -140,7 +140,7 @@ fun cert_class (TSig {classes, ...}) = Sorts.certify_class (#2 classes); fun cert_sort (TSig {classes, ...}) = Sorts.certify_sort (#2 classes); -fun witness_sorts (tsig as TSig {classes, log_types, ...}) = +fun witness_sorts (TSig {classes, log_types, ...}) = Sorts.witness_sorts (#2 classes) log_types; @@ -280,7 +280,7 @@ val used = Name.context |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t; val fmap = fs ~~ map (rpair 0) (#1 (Name.variants (map fst fs) used)); - fun thaw (f as (a, S)) = + fun thaw (f as (_, S)) = (case AList.lookup (op =) fmap f of NONE => TFree f | SOME xi => TVar (xi, S)); @@ -412,10 +412,10 @@ (case lookup tye v of SOME U => devar tye U | NONE => T) - | devar tye T = T; + | devar _ T = T; (*order-sorted unification*) -fun unify (tsig as TSig {classes = (_, classes), ...}) TU (tyenv, maxidx) = +fun unify (TSig {classes = (_, classes), ...}) TU (tyenv, maxidx) = let val tyvar_count = Unsynchronized.ref maxidx; fun gen_tyvar S = TVar ((Name.aT, Unsynchronized.inc tyvar_count), S); @@ -465,7 +465,7 @@ (*purely structural unification*) fun raw_unify (ty1, ty2) tye = (case (devar tye ty1, devar tye ty2) of - (T as TVar (v, S1), U as TVar (w, S2)) => + (T as TVar (v, S1), TVar (w, S2)) => if Term.eq_ix (v, w) then if S1 = S2 then tye else tvar_clash v S1 S2 else Vartab.update_new (w, (S2, T)) tye @@ -545,7 +545,7 @@ let val rel' = pairself (cert_class tsig) rel handle TYPE (msg, _, _) => error msg; - val classes' = classes |> Sorts.add_classrel pp rel; + val classes' = classes |> Sorts.add_classrel pp rel'; in ((space, classes'), default, types) end); diff -r e43d761a742d -r 1a5dde5079ac src/Pure/variable.ML --- a/src/Pure/variable.ML Wed Sep 30 19:04:48 2009 +0200 +++ b/src/Pure/variable.ML Wed Sep 30 22:20:58 2009 +0200 @@ -89,7 +89,7 @@ structure Data = ProofDataFun ( type T = data; - fun init thy = + fun init _ = make_data (false, Name.context, Symtab.empty, [], Vartab.empty, Symtab.empty, ~1, [], (Vartab.empty, Vartab.empty)); );