--- a/src/HOL/Import/proof_kernel.ML Sun Mar 04 00:04:37 2012 +0100
+++ b/src/HOL/Import/proof_kernel.ML Sun Mar 04 00:15:08 2012 +0100
@@ -116,7 +116,7 @@
val replay_add_dump : string -> theory -> theory
end
-structure ProofKernel :> ProofKernel =
+structure ProofKernel : ProofKernel =
struct
type hol_type = Term.typ
type term = Term.term
@@ -243,7 +243,7 @@
val topctxt = ML_Context.the_local_context ();
fun prin t = writeln (Print_Mode.setmp []
(fn () => Syntax.string_of_term topctxt t) ());
-fun pth (HOLThm(ren,thm)) =
+fun pth (HOLThm(_,thm)) =
let
(*val _ = writeln "Renaming:"
val _ = app (fn(v,w) => (prin v; writeln " -->"; prin w)) ren*)
@@ -349,7 +349,7 @@
fun mk_thy_const thy Thy Nam Ty = Const(intern_const_name Thy Nam thy,Ty)
local
- fun get_const sg thyname name =
+ fun get_const sg _ name =
(case Sign.const_type sg name of
SOME ty => Const (name, ty)
| NONE => raise ERR "get_type" (name ^ ": No such constant"))
@@ -430,7 +430,7 @@
let
val xl = raw_explode x
val yl = raw_explode y
- fun isprefix [] ys = true
+ fun isprefix [] _ = true
| isprefix (x::xs) (y::ys) = if x = y then isprefix xs ys else false
| isprefix _ _ = false
fun isp s = isprefix xl s
@@ -497,7 +497,7 @@
gtfx
end
-fun input_types thyname (Elem("tylist",[("i",i)],xtys)) =
+fun input_types _ (Elem("tylist",[("i",i)],xtys)) =
let
val types = Array.array(the (Int.fromString i),XMLty (Elem("",[],[])))
fun IT _ [] = ()
@@ -528,10 +528,6 @@
| NONE => raise ERR "get_term_from_index" "Bad index"
and get_term_from_xml thy thyname types terms =
let
- fun get_type [] = NONE
- | get_type [ty] = SOME (TypeNet.get_type_from_xml thy thyname types ty)
- | get_type _ = raise ERR "get_term" "Bad type"
-
fun gtfx (Elem("tmv",[("n",name),("t",tyi)],[])) =
mk_var(protect_varname name,TypeNet.get_type_from_index thy thyname types tyi)
| gtfx (Elem("tmc",atts,[])) =
@@ -564,7 +560,7 @@
gtfx
end
-fun input_terms thyname types (Elem("tmlist",[("i",i)],xtms)) =
+fun input_terms _ _ (Elem("tmlist",[("i",i)],xtms)) =
let
val terms = Array.array(the (Int.fromString i), XMLtm (Elem("",[],[])))
@@ -684,10 +680,10 @@
end
| x2p (Elem("ptydef",[("s",seg),("n",name)],[p])) =
mk_proof (PTyDef(seg,protect_tyname name,x2p p))
- | x2p (xml as Elem("poracle",[],chldr)) =
+ | x2p (Elem("poracle",[],chldr)) =
let
val (oracles,terms) = List.partition (fn (Elem("oracle",_,_)) => true | _ => false) chldr
- val ors = map (fn (Elem("oracle",[("n",name)],[])) => name | xml => raise ERR "x2p" "bad oracle") oracles
+ val ors = map (fn (Elem("oracle",[("n",name)],[])) => name | _ => raise ERR "x2p" "bad oracle") oracles
val (c,asl) = case terms of
[] => raise ERR "x2p" "Bad oracle description"
| (hd::tl) => (hd,tl)
@@ -846,7 +842,7 @@
in
mk_proof (PContr (p,t))
end
- | x2p xml = raise ERR "x2p" "Bad proof"
+ | x2p _ = raise ERR "x2p" "Bad proof"
in
x2p prf
end
@@ -858,7 +854,7 @@
val _ = TextIO.closeIn is
in
case proof_xml of
- Elem("proof",[],xtypes::xterms::prf::rest) =>
+ Elem("proof",[],xtypes::xterms::_::rest) =>
let
val types = TypeNet.input_types thyname xtypes
val terms = TermNet.input_terms thyname types xterms
@@ -971,9 +967,9 @@
val c = prop_of th3
val vname = fst(dest_Free v)
val (cold,cnew) = case c of
- tpc $ (Const(@{const_name All},allT) $ Abs(oldname,ty,body)) =>
+ tpc $ (Const(@{const_name All},_) $ Abs(oldname,_,_)) =>
(Abs(oldname,dummyT,Bound 0),Abs(vname,dummyT,Bound 0))
- | tpc $ (Const(@{const_name All},allT) $ rest) => (tpc,tpc)
+ | tpc $ (Const(@{const_name All},_) $ _) => (tpc,tpc)
| _ => raise ERR "mk_GEN" "Unknown conclusion"
val th4 = Thm.rename_boundvars cold cnew th3
val res = implies_intr_hyps th4
@@ -1004,7 +1000,7 @@
val disamb_info_empty = {vars=[],rens=[]}
-fun rens_of {vars,rens} = rens
+fun rens_of { vars = _, rens = rens } = rens
fun disamb_term_from info tm = (info, tm)
@@ -1020,7 +1016,7 @@
fun disamb_thm thm = disamb_thm_from disamb_info_empty thm
fun disamb_thms thms = disamb_thms_from disamb_info_empty thms
-fun norm_hthm thy (hth as HOLThm _) = hth
+fun norm_hthm _ (hth as HOLThm _) = hth
(* End of disambiguating code *)
@@ -1043,7 +1039,7 @@
n'
end
val new_name = new_name' "a"
- fun replace_name n' (Free (n, t)) = Free (n', t)
+ fun replace_name n' (Free (_, t)) = Free (n', t)
| replace_name _ _ = ERR "replace_name"
(* map: old or fresh name -> old free,
invmap: old free which has fresh name assigned to it -> fresh name *)
@@ -1187,7 +1183,7 @@
val (a, b) = get_isabelle_thm thyname thmname importerconc thy
fun warn () =
let
- val (info,importerconc') = disamb_term importerconc
+ val (_,importerconc') = disamb_term importerconc
val i2h_conc = Thm.symmetric (rewrite_importer_term (HOLogic.mk_Trueprop importerconc') thy)
in
case concl_of i2h_conc of
@@ -1211,8 +1207,8 @@
| NONE => ((case import_proof_concl thyname thmname thy of
SOME f => get_isabelle_thm_and_warn thyname thmname (f thy) thy
| NONE => (message "No conclusion"; (thy,NONE)))
- handle e as IO.Io _ => (message "IO exception"; (thy,NONE))
- | e as PK _ => (message "PK exception"; (thy,NONE)))
+ handle IO.Io _ => (message "IO exception"; (thy,NONE))
+ | PK _ => (message "PK exception"; (thy,NONE)))
fun rename_const thyname thy name =
case get_importer_const_renaming thyname name thy of
@@ -1284,7 +1280,7 @@
(thy,res)
end
-fun INST_TYPE lambda (hth as HOLThm(rens,th)) thy =
+fun INST_TYPE lambda (hth as HOLThm(_,th)) thy =
let
val _ = message "INST_TYPE:"
val _ = if_debug pth hth
@@ -1699,7 +1695,7 @@
val (info',vlist') = disamb_terms_from info vlist
val th1 =
case copt of
- SOME (c as Const(cname,cty)) =>
+ SOME (Const(cname,cty)) =>
let
fun inst_type ty1 ty2 (TVar _) = raise ERR "GEN_ABS" "Type variable found!"
| inst_type ty1 ty2 (ty as TFree _) = if ty1 = ty
@@ -1788,7 +1784,7 @@
val redeclared = is_some (Sign.const_type thy (Sign.intern_const thy constname));
val _ = warning ("Introducing constant " ^ constname)
val (thmname,thy) = get_defname thyname constname thy
- val (info,rhs') = disamb_term rhs
+ val (_,rhs') = disamb_term rhs
val ctype = type_of rhs'
val csyn = mk_syn thy constname
val thy1 = case Importer_DefThy.get thy of
@@ -1859,14 +1855,14 @@
fun dest_eta_abs (Abs(x,xT,body)) = (x,xT,body)
| dest_eta_abs body =
let
- val (dT,rT) = Term.dest_funT (type_of body)
+ val (dT,_) = Term.dest_funT (type_of body)
in
("x",dT,body $ Bound 0)
end
handle TYPE _ => raise ERR "new_specification" "not an abstraction type"
fun dest_exists (Const(@{const_name Ex},_) $ abody) =
dest_eta_abs abody
- | dest_exists tm =
+ | dest_exists _ =
raise ERR "new_specification" "Bad existential formula"
val (consts,_) = Library.foldl (fn ((cs,ex),cname) =>
@@ -1920,7 +1916,7 @@
intern_store_thm false thyname thmname hth thy''
end
-fun new_axiom name tm thy = raise ERR "new_axiom" ("Oh, no you don't! (" ^ name ^ ")")
+fun new_axiom name _ _ = raise ERR "new_axiom" ("Oh, no you don't! (" ^ name ^ ")")
fun to_isa_thm (hth as HOLThm(_,th)) =
let
--- a/src/HOL/Import/shuffler.ML Sun Mar 04 00:04:37 2012 +0100
+++ b/src/HOL/Import/shuffler.ML Sun Mar 04 00:15:08 2012 +0100
@@ -27,7 +27,7 @@
val setup : theory -> theory
end
-structure Shuffler :> Shuffler =
+structure Shuffler : Shuffler =
struct
val debug = Unsynchronized.ref false
@@ -57,7 +57,6 @@
val PQ = Logic.mk_implies(P,Q)
val PPQ = Logic.mk_implies(P,PQ)
val cP = cert P
- val cQ = cert Q
val cPQ = cert PQ
val cPPQ = cert PPQ
val th1 = Thm.assume cPQ |> implies_intr_list [cPQ,cP]
@@ -150,7 +149,7 @@
| swap_bound n (Abs(x,xT,t)) = Abs(x,xT,swap_bound (n+1) t)
| swap_bound n t = t
-fun rew_th thy (xv as (x,xT)) (yv as (y,yT)) t =
+fun rew_th thy xv yv t =
let
val lhs = Logic.list_all ([xv,yv],t)
val rhs = Logic.list_all ([yv,xv],swap_bound 0 t)
@@ -306,7 +305,7 @@
Const("==",T) $ P $ Q =>
if is_Abs P orelse is_Abs Q
then (case domain_type T of
- Type("fun",[aT,bT]) =>
+ Type("fun",[aT,_]) =>
let
val cert = cterm_of thy
val vname = singleton (Name.variant_list (Term.add_free_names t [])) "v"
@@ -345,8 +344,6 @@
val P = mk_free "P" (xT-->yT-->propT)
val Q = mk_free "Q" (xT-->yT)
val R = mk_free "R" (xT-->yT)
-val S = mk_free "S" xT
-val S' = mk_free "S'" xT
in
fun quant_simproc thy = Simplifier.simproc_global_i
@@ -379,7 +376,7 @@
in
(t' $ u',idx'')
end
- | F (Abs(x,xT,t),idx) =
+ | F (Abs(_,xT,t),idx) =
let
val x' = "x" ^ string_of_int idx
val (t',idx') = F (t,idx+1)
@@ -458,7 +455,7 @@
in
SOME th
end
- handle e as THM _ => (message "make_equal: NONE";NONE)
+ handle THM _ => (message "make_equal: NONE";NONE)
fun match_consts ignore t (* th *) =
let
@@ -471,7 +468,7 @@
| add_consts (_, cs) = cs
val t_consts = add_consts(t,[])
in
- fn (name,th) =>
+ fn (_,th) =>
let
val th_consts = add_consts(prop_of th,[])
in
@@ -521,11 +518,11 @@
end
| NONE => process thms
end
- handle e as THM _ => process thms
+ handle THM _ => process thms
in
fn thms =>
case process thms of
- res as SOME (name,th) => if (prop_of th) aconv t
+ res as SOME (_,th) => if (prop_of th) aconv t
then res
else error "Internal error in set_prop"
| NONE => NONE