removed some unreferenced material;
authorwenzelm
Sun Oct 18 20:53:40 2009 +0200 (2009-10-18)
changeset 32994ccc07fbbfefd
parent 32993 078c1f7fa8be
child 32995 304a841fd39c
removed some unreferenced material;
tuned;
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_hol_clause.ML
src/HOL/Tools/res_reconstruct.ML
     1.1 --- a/src/HOL/Tools/metis_tools.ML	Sun Oct 18 18:08:04 2009 +0200
     1.2 +++ b/src/HOL/Tools/metis_tools.ML	Sun Oct 18 20:53:40 2009 +0200
     1.3 @@ -81,11 +81,11 @@
     1.4      | (ResHolClause.CombVar(v,_), []) => Metis.Term.Var v
     1.5      | _ => error "hol_term_to_fol_FO";
     1.6  
     1.7 -fun hol_term_to_fol_HO (ResHolClause.CombVar(a, ty)) = Metis.Term.Var a
     1.8 -  | hol_term_to_fol_HO (ResHolClause.CombConst(a, ty, tylist)) =
     1.9 -      Metis.Term.Fn(fn_isa_to_met a, map hol_type_to_fol tylist)
    1.10 -  | hol_term_to_fol_HO (ResHolClause.CombApp(tm1,tm2)) =
    1.11 -       Metis.Term.Fn(".", map hol_term_to_fol_HO [tm1,tm2]);
    1.12 +fun hol_term_to_fol_HO (ResHolClause.CombVar (a, _)) = Metis.Term.Var a
    1.13 +  | hol_term_to_fol_HO (ResHolClause.CombConst (a, _, tylist)) =
    1.14 +      Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
    1.15 +  | hol_term_to_fol_HO (ResHolClause.CombApp (tm1, tm2)) =
    1.16 +       Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
    1.17  
    1.18  (*The fully-typed translation, to avoid type errors*)
    1.19  fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
    1.20 @@ -122,8 +122,8 @@
    1.21  fun metis_of_typeLit pos (ResClause.LTVar (s,x))  = metis_lit pos s [Metis.Term.Var x]
    1.22    | metis_of_typeLit pos (ResClause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
    1.23  
    1.24 -fun default_sort ctxt (TVar _) = false
    1.25 -  | default_sort ctxt (TFree(x,s)) = (s = Option.getOpt (Variable.def_sort ctxt (x,~1), []));
    1.26 +fun default_sort _ (TVar _) = false
    1.27 +  | default_sort ctxt (TFree (x, s)) = (s = Option.getOpt (Variable.def_sort ctxt (x, ~1), []));
    1.28  
    1.29  fun metis_of_tfree tf =
    1.30    Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf));
    1.31 @@ -162,7 +162,7 @@
    1.32  fun m_classrel_cls subclass superclass =
    1.33    [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
    1.34  
    1.35 -fun classrel_cls (ResClause.ClassrelClause {axiom_name,subclass,superclass,...}) =
    1.36 +fun classrel_cls (ResClause.ClassrelClause {subclass, superclass, ...}) =
    1.37    (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
    1.38  
    1.39  (* ------------------------------------------------------------------------- *)
    1.40 @@ -176,10 +176,10 @@
    1.41    | terms_of (Type _ :: tts) = terms_of tts;
    1.42  
    1.43  fun types_of [] = []
    1.44 -  | types_of (Term (Term.Var((a,idx), T)) :: tts) =
    1.45 +  | types_of (Term (Term.Var ((a,idx), _)) :: tts) =
    1.46        if String.isPrefix "_" a then
    1.47            (*Variable generated by Metis, which might have been a type variable.*)
    1.48 -          TVar(("'" ^ a, idx), HOLogic.typeS) :: types_of tts
    1.49 +          TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
    1.50        else types_of tts
    1.51    | types_of (Term _ :: tts) = types_of tts
    1.52    | types_of (Type T :: tts) = T :: types_of tts;
    1.53 @@ -210,7 +210,7 @@
    1.54  fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
    1.55    | strip_happ args x = (x, args);
    1.56  
    1.57 -fun fol_type_to_isa ctxt (Metis.Term.Var v) =
    1.58 +fun fol_type_to_isa _ (Metis.Term.Var v) =
    1.59       (case Recon.strip_prefix ResClause.tvar_prefix v of
    1.60            SOME w => Recon.make_tvar w
    1.61          | NONE   => Recon.make_tvar v)
    1.62 @@ -281,11 +281,11 @@
    1.63  (*Maps fully-typed metis terms to isabelle terms*)
    1.64  fun fol_term_to_hol_FT ctxt fol_tm =
    1.65    let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
    1.66 -      fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, ty])) =
    1.67 +      fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
    1.68               (case Recon.strip_prefix ResClause.schematic_var_prefix v of
    1.69                    SOME w =>  mk_var(w, dummyT)
    1.70                  | NONE   => mk_var(v, dummyT))
    1.71 -        | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), ty])) =
    1.72 +        | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
    1.73              Const ("op =", HOLogic.typeT)
    1.74          | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
    1.75             (case Recon.strip_prefix ResClause.const_prefix x of
    1.76 @@ -356,7 +356,7 @@
    1.77    in  cterm_instantiate substs th  end;
    1.78  
    1.79  (* INFERENCE RULE: AXIOM *)
    1.80 -fun axiom_inf ctxt thpairs th = incr_indexes 1 (lookth thpairs th);
    1.81 +fun axiom_inf thpairs th = incr_indexes 1 (lookth thpairs th);
    1.82      (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
    1.83  
    1.84  (* INFERENCE RULE: ASSUME *)
    1.85 @@ -418,7 +418,6 @@
    1.86  
    1.87  fun resolve_inf ctxt mode thpairs atm th1 th2 =
    1.88    let
    1.89 -    val thy = ProofContext.theory_of ctxt
    1.90      val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
    1.91      val _ = trace_msg (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
    1.92      val _ = trace_msg (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
    1.93 @@ -451,17 +450,17 @@
    1.94        val c_t = cterm_incr_types thy refl_idx i_t
    1.95    in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
    1.96  
    1.97 -fun get_ty_arg_size thy (Const("op =",_)) = 0  (*equality has no type arguments*)
    1.98 -  | get_ty_arg_size thy (Const(c,_))      = (Recon.num_typargs thy c handle TYPE _ => 0)
    1.99 -  | get_ty_arg_size thy _      = 0;
   1.100 +fun get_ty_arg_size _ (Const ("op =", _)) = 0  (*equality has no type arguments*)
   1.101 +  | get_ty_arg_size thy (Const (c, _)) = (Recon.num_typargs thy c handle TYPE _ => 0)
   1.102 +  | get_ty_arg_size _ _ = 0;
   1.103  
   1.104  (* INFERENCE RULE: EQUALITY *)
   1.105 -fun equality_inf ctxt mode thpairs (pos,atm) fp fr =
   1.106 +fun equality_inf ctxt mode (pos, atm) fp fr =
   1.107    let val thy = ProofContext.theory_of ctxt
   1.108        val m_tm = Metis.Term.Fn atm
   1.109        val [i_atm,i_tm] = fol_terms_to_hol ctxt mode [m_tm, fr]
   1.110        val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
   1.111 -      fun replace_item_list lx 0 (l::ls) = lx::ls
   1.112 +      fun replace_item_list lx 0 (_::ls) = lx::ls
   1.113          | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
   1.114        fun path_finder_FO tm [] = (tm, Term.Bound 0)
   1.115          | path_finder_FO tm (p::ps) =
   1.116 @@ -479,13 +478,13 @@
   1.117              end
   1.118        fun path_finder_HO tm [] = (tm, Term.Bound 0)
   1.119          | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
   1.120 -        | path_finder_HO (t$u) (p::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
   1.121 +        | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
   1.122        fun path_finder_FT tm [] _ = (tm, Term.Bound 0)
   1.123 -        | path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1,t2])) =
   1.124 +        | path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1, _])) =
   1.125              path_finder_FT tm ps t1
   1.126 -        | path_finder_FT (t$u) (0::ps) (Metis.Term.Fn (".", [t1,t2])) =
   1.127 +        | path_finder_FT (t$u) (0::ps) (Metis.Term.Fn (".", [t1, _])) =
   1.128              (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
   1.129 -        | path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [t1,t2])) =
   1.130 +        | path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [_, t2])) =
   1.131              (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
   1.132          | path_finder_FT tm ps t = error ("equality_inf, path_finder_FT: path = " ^
   1.133                                          space_implode " " (map Int.toString ps) ^
   1.134 @@ -496,7 +495,7 @@
   1.135               (*equality: not curried, as other predicates are*)
   1.136               if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
   1.137               else path_finder_HO tm (p::ps)        (*1 selects second operand*)
   1.138 -        | path_finder HO tm (p::ps) (Metis.Term.Fn ("{}", [t1])) =
   1.139 +        | path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) =
   1.140               path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
   1.141          | path_finder FT (tm as Const("op =",_) $ _ $ _) (p::ps)
   1.142                              (Metis.Term.Fn ("=", [t1,t2])) =
   1.143 @@ -507,7 +506,7 @@
   1.144               else path_finder_FT tm (p::ps)
   1.145                     (Metis.Term.Fn (".", [metis_eq,t2]))
   1.146                     (*1 selects second operand*)
   1.147 -        | path_finder FT tm (p::ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
   1.148 +        | path_finder FT tm (_ :: ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
   1.149               (*if not equality, ignore head to skip the hBOOL predicate*)
   1.150          | path_finder FT tm ps t = path_finder_FT tm ps t  (*really an error case!*)
   1.151        fun path_finder_lit ((nt as Term.Const ("Not", _)) $ tm_a) idx =
   1.152 @@ -528,22 +527,19 @@
   1.153  
   1.154  val factor = Seq.hd o distinct_subgoals_tac;
   1.155  
   1.156 -fun step ctxt mode thpairs (fol_th, Metis.Proof.Axiom _)                        =
   1.157 -      factor (axiom_inf ctxt thpairs fol_th)
   1.158 -  | step ctxt mode thpairs (_, Metis.Proof.Assume f_atm)                        =
   1.159 -      assume_inf ctxt mode f_atm
   1.160 -  | step ctxt mode thpairs (_, Metis.Proof.Subst(f_subst, f_th1))               =
   1.161 +fun step _ _ thpairs (fol_th, Metis.Proof.Axiom _) = factor (axiom_inf thpairs fol_th)
   1.162 +  | step ctxt mode _ (_, Metis.Proof.Assume f_atm) = assume_inf ctxt mode f_atm
   1.163 +  | step ctxt mode thpairs (_, Metis.Proof.Subst (f_subst, f_th1)) =
   1.164        factor (inst_inf ctxt mode thpairs f_subst f_th1)
   1.165 -  | step ctxt mode thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2))        =
   1.166 +  | step ctxt mode thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) =
   1.167        factor (resolve_inf ctxt mode thpairs f_atm f_th1 f_th2)
   1.168 -  | step ctxt mode thpairs (_, Metis.Proof.Refl f_tm)                           =
   1.169 -      refl_inf ctxt mode f_tm
   1.170 -  | step ctxt mode thpairs (_, Metis.Proof.Equality(f_lit, f_p, f_r)) =
   1.171 -      equality_inf ctxt mode thpairs f_lit f_p f_r;
   1.172 +  | step ctxt mode _ (_, Metis.Proof.Refl f_tm) = refl_inf ctxt mode f_tm
   1.173 +  | step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =
   1.174 +      equality_inf ctxt mode f_lit f_p f_r;
   1.175  
   1.176 -fun real_literal (b, (c, _)) = not (String.isPrefix ResClause.class_prefix c);
   1.177 +fun real_literal (_, (c, _)) = not (String.isPrefix ResClause.class_prefix c);
   1.178  
   1.179 -fun translate mode _    thpairs [] = thpairs
   1.180 +fun translate _ _ thpairs [] = thpairs
   1.181    | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
   1.182        let val _ = trace_msg (fn () => "=============================================")
   1.183            val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
   1.184 @@ -551,7 +547,8 @@
   1.185            val th = Meson.flexflex_first_order (step ctxt mode thpairs (fol_th, inf))
   1.186            val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
   1.187            val _ = trace_msg (fn () => "=============================================")
   1.188 -          val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
   1.189 +          val n_metis_lits =
   1.190 +            length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
   1.191        in
   1.192            if nprems_of th = n_metis_lits then ()
   1.193            else error "Metis: proof reconstruction has gone wrong";
   1.194 @@ -560,7 +557,7 @@
   1.195  
   1.196  (*Determining which axiom clauses are actually used*)
   1.197  fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th)
   1.198 -  | used_axioms axioms _                         = NONE;
   1.199 +  | used_axioms _ _ = NONE;
   1.200  
   1.201  (* ------------------------------------------------------------------------- *)
   1.202  (* Translation of HO Clauses                                                 *)
   1.203 @@ -581,8 +578,7 @@
   1.204    let val subs = ResAtp.tfree_classes_of_terms tms
   1.205        val supers = ResAtp.tvar_classes_of_terms tms
   1.206        and tycons = ResAtp.type_consts_of_terms thy tms
   1.207 -      val arity_clauses = ResClause.make_arity_clauses thy tycons supers
   1.208 -      val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
   1.209 +      val (supers', arity_clauses) = ResClause.make_arity_clauses thy tycons supers
   1.210        val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   1.211    in  map classrel_cls classrel_clauses @ map arity_cls arity_clauses
   1.212    end;
   1.213 @@ -595,12 +591,12 @@
   1.214    {axioms : (Metis.Thm.thm * Thm.thm) list,
   1.215     tfrees : ResClause.type_literal list};
   1.216  
   1.217 -fun const_in_metis c (pol,(pred,tm_list)) =
   1.218 +fun const_in_metis c (pred, tm_list) =
   1.219    let
   1.220 -    fun in_mterm (Metis.Term.Var nm) = false
   1.221 +    fun in_mterm (Metis.Term.Var _) = false
   1.222        | in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list
   1.223        | in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
   1.224 -  in  c=pred orelse exists in_mterm tm_list  end;
   1.225 +  in  c = pred orelse exists in_mterm tm_list  end;
   1.226  
   1.227  (*Extract TFree constraints from context to include as conjecture clauses*)
   1.228  fun init_tfrees ctxt =
   1.229 @@ -641,7 +637,7 @@
   1.230                          {axioms = [], tfrees = init_tfrees ctxt} cls
   1.231        val lmap = List.foldl (add_thm false) (add_tfrees lmap0) ths
   1.232        val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
   1.233 -      fun used c = exists (Metis.LiteralSet.exists (const_in_metis c)) clause_lists
   1.234 +      fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
   1.235        (*Now check for the existence of certain combinators*)
   1.236        val thI  = if used "c_COMBI" then [comb_I] else []
   1.237        val thK  = if used "c_COMBK" then [comb_K] else []
   1.238 @@ -697,7 +693,7 @@
   1.239                  and used = map_filter (used_axioms axioms) proof
   1.240                  val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
   1.241                  val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
   1.242 -                val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs
   1.243 +                val unused = filter (fn (_, cls) => not (common_thm used cls)) th_cls_pairs
   1.244              in
   1.245                  if null unused then ()
   1.246                  else warning ("Metis: unused theorems " ^ commas_quote (map #1 unused));
     2.1 --- a/src/HOL/Tools/res_atp.ML	Sun Oct 18 18:08:04 2009 +0200
     2.2 +++ b/src/HOL/Tools/res_atp.ML	Sun Oct 18 20:53:40 2009 +0200
     2.3 @@ -112,7 +112,7 @@
     2.4    | add_term_consts_typs_rm thy (t $ u, tab) =
     2.5        add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (u, tab))
     2.6    | add_term_consts_typs_rm thy (Abs(_,_,t), tab) = add_term_consts_typs_rm thy (t, tab)
     2.7 -  | add_term_consts_typs_rm thy (_, tab) = tab;
     2.8 +  | add_term_consts_typs_rm _ (_, tab) = tab;
     2.9  
    2.10  (*The empty list here indicates that the constant is being ignored*)
    2.11  fun add_standard_const (s,tab) = Symtab.update (s,[]) tab;
    2.12 @@ -208,7 +208,7 @@
    2.13    | dest_ConstFree _ = raise ConstFree;
    2.14  
    2.15  (*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
    2.16 -fun defines thy (thm,(name,n)) gctypes =
    2.17 +fun defines thy thm gctypes =
    2.18      let val tm = prop_of thm
    2.19          fun defs lhs rhs =
    2.20              let val (rator,args) = strip_comb lhs
    2.21 @@ -262,7 +262,7 @@
    2.22          | relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) =
    2.23              let val weight = clause_weight ctab rel_consts consts_typs
    2.24              in
    2.25 -              if p <= weight orelse (follow_defs andalso defines thy clsthm rel_consts)
    2.26 +              if p <= weight orelse (follow_defs andalso defines thy (#1 clsthm) rel_consts)
    2.27                then (ResAxioms.trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^ 
    2.28                                              " passes: " ^ Real.toString weight));
    2.29                      relevant ((ax,weight)::newrels, rejects) axs)
    2.30 @@ -403,7 +403,7 @@
    2.31  
    2.32  fun check_named ("", th) =
    2.33        (warning ("No name for theorem " ^ Display.string_of_thm_without_context th); false)
    2.34 -  | check_named (_, th) = true;
    2.35 +  | check_named _ = true;
    2.36  
    2.37  (* get lemmas from claset, simpset, atpset and extra supplied rules *)
    2.38  fun get_clasimp_atp_lemmas ctxt =
    2.39 @@ -440,7 +440,7 @@
    2.40  
    2.41  (*fold type constructors*)
    2.42  fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
    2.43 -  | fold_type_consts f T x = x;
    2.44 +  | fold_type_consts _ _ x = x;
    2.45  
    2.46  val add_type_consts_in_type = fold_type_consts setinsert;
    2.47  
    2.48 @@ -448,7 +448,7 @@
    2.49  fun add_type_consts_in_term thy =
    2.50    let val const_typargs = Sign.const_typargs thy
    2.51        fun add_tcs (Const cT) x = fold add_type_consts_in_type (const_typargs cT) x
    2.52 -        | add_tcs (Abs (_, T, u)) x = add_tcs u x
    2.53 +        | add_tcs (Abs (_, _, u)) x = add_tcs u x
    2.54          | add_tcs (t $ u) x = add_tcs t (add_tcs u x)
    2.55          | add_tcs _ x = x
    2.56    in  add_tcs  end
     3.1 --- a/src/HOL/Tools/res_axioms.ML	Sun Oct 18 18:08:04 2009 +0200
     3.2 +++ b/src/HOL/Tools/res_axioms.ML	Sun Oct 18 20:53:40 2009 +0200
     3.3 @@ -91,7 +91,7 @@
     3.4              val thy'' = Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
     3.5              val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef)
     3.6            in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
     3.7 -      | dec_sko (Const ("All", _) $ (xtp as Abs (a, T, p))) thx =
     3.8 +      | dec_sko (Const ("All", _) $ (Abs (a, T, p))) thx =
     3.9            (*Universal quant: insert a free variable into body and continue*)
    3.10            let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
    3.11            in dec_sko (subst_bound (Free (fname, T), p)) thx end
    3.12 @@ -119,7 +119,7 @@
    3.13              in dec_sko (subst_bound (list_comb(c,args), p))
    3.14                         (def :: defs)
    3.15              end
    3.16 -        | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) defs =
    3.17 +        | dec_sko (Const ("All",_) $ Abs (a, T, p)) defs =
    3.18              (*Universal quant: insert a free variable into body and continue*)
    3.19              let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
    3.20              in dec_sko (subst_bound (Free(fname,T), p)) defs end
    3.21 @@ -158,8 +158,6 @@
    3.22  
    3.23  val lambda_free = not o Term.has_abs;
    3.24  
    3.25 -val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar);
    3.26 -
    3.27  val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B}));
    3.28  val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
    3.29  val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
    3.30 @@ -216,14 +214,14 @@
    3.31    else
    3.32    case term_of ct of
    3.33        Abs _ =>
    3.34 -        let val (cv,cta) = Thm.dest_abs NONE ct
    3.35 -            val (v,Tv) = (dest_Free o term_of) cv
    3.36 +        let val (cv, cta) = Thm.dest_abs NONE ct
    3.37 +            val (v, _) = dest_Free (term_of cv)
    3.38              val u_th = combinators_aux cta
    3.39              val cu = Thm.rhs_of u_th
    3.40              val comb_eq = abstract (Thm.cabs cv cu)
    3.41          in transitive (abstract_rule v cv u_th) comb_eq end
    3.42 -    | t1 $ t2 =>
    3.43 -        let val (ct1,ct2) = Thm.dest_comb ct
    3.44 +    | _ $ _ =>
    3.45 +        let val (ct1, ct2) = Thm.dest_comb ct
    3.46          in  combination (combinators_aux ct1) (combinators_aux ct2)  end;
    3.47  
    3.48  fun combinators th =
    3.49 @@ -286,11 +284,6 @@
    3.50  fun assume_skolem_of_def s th =
    3.51    map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
    3.52  
    3.53 -fun assert_lambda_free ths msg =
    3.54 -  case filter (not o lambda_free o prop_of) ths of
    3.55 -      [] => ()
    3.56 -    | ths' => error (cat_lines (msg :: map Display.string_of_thm_without_context ths'));
    3.57 -
    3.58  
    3.59  (*** Blacklisting (duplicated in ResAtp?) ***)
    3.60  
    3.61 @@ -343,10 +336,6 @@
    3.62    if Thm.has_name_hint th then flatten_name (Thm.get_name_hint th)
    3.63    else gensym "unknown_thm_";
    3.64  
    3.65 -fun name_or_string th =
    3.66 -  if Thm.has_name_hint th then Thm.get_name_hint th
    3.67 -  else Display.string_of_thm_without_context th;
    3.68 -
    3.69  (*Skolemize a named theorem, with Skolem functions as additional premises.*)
    3.70  fun skolem_thm (s, th) =
    3.71    if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse bad_for_atp th then []
     4.1 --- a/src/HOL/Tools/res_hol_clause.ML	Sun Oct 18 18:08:04 2009 +0200
     4.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Sun Oct 18 20:53:40 2009 +0200
     4.3 @@ -119,9 +119,9 @@
     4.4  fun type_of dfg (Type (a, Ts)) =
     4.5        let val (folTypes,ts) = types_of dfg Ts
     4.6        in  (RC.Comp(RC.make_fixed_type_const dfg a, folTypes), ts)  end
     4.7 -  | type_of dfg (tp as (TFree(a,s))) =
     4.8 +  | type_of _ (tp as TFree (a, _)) =
     4.9        (RC.AtomF (RC.make_fixed_type_var a), [tp])
    4.10 -  | type_of dfg (tp as (TVar(v,s))) =
    4.11 +  | type_of _ (tp as TVar (v, _)) =
    4.12        (RC.AtomV (RC.make_schematic_type_var v), [tp])
    4.13  and types_of dfg Ts =
    4.14        let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
    4.15 @@ -130,8 +130,8 @@
    4.16  (* same as above, but no gathering of sort information *)
    4.17  fun simp_type_of dfg (Type (a, Ts)) =
    4.18        RC.Comp(RC.make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
    4.19 -  | simp_type_of dfg (TFree (a,s)) = RC.AtomF(RC.make_fixed_type_var a)
    4.20 -  | simp_type_of dfg (TVar (v,s)) = RC.AtomV(RC.make_schematic_type_var v);
    4.21 +  | simp_type_of _ (TFree (a, _)) = RC.AtomF(RC.make_fixed_type_var a)
    4.22 +  | simp_type_of _ (TVar (v, _)) = RC.AtomV(RC.make_schematic_type_var v);
    4.23  
    4.24  
    4.25  fun const_type_of dfg thy (c,t) =
    4.26 @@ -143,11 +143,11 @@
    4.27        let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t)
    4.28            val c' = CombConst(RC.make_fixed_const dfg c, tp, tvar_list)
    4.29        in  (c',ts)  end
    4.30 -  | combterm_of dfg thy (Free(v,t)) =
    4.31 +  | combterm_of dfg _ (Free(v,t)) =
    4.32        let val (tp,ts) = type_of dfg t
    4.33            val v' = CombConst(RC.make_fixed_var v, tp, [])
    4.34        in  (v',ts)  end
    4.35 -  | combterm_of dfg thy (Var(v,t)) =
    4.36 +  | combterm_of dfg _ (Var(v,t)) =
    4.37        let val (tp,ts) = type_of dfg t
    4.38            val v' = CombVar(RC.make_schematic_var v,tp)
    4.39        in  (v',ts)  end
    4.40 @@ -155,7 +155,7 @@
    4.41        let val (P',tsP) = combterm_of dfg thy P
    4.42            val (Q',tsQ) = combterm_of dfg thy Q
    4.43        in  (CombApp(P',Q'), tsP union tsQ)  end
    4.44 -  | combterm_of _ thy (t as Abs _) = raise RC.CLAUSE("HOL CLAUSE",t);
    4.45 +  | combterm_of _ _ (t as Abs _) = raise RC.CLAUSE ("HOL CLAUSE", t);
    4.46  
    4.47  fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity)
    4.48    | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity);
    4.49 @@ -195,7 +195,7 @@
    4.50  
    4.51  fun make_axiom_clauses dfg thy = List.foldl (add_axiom_clause dfg thy) [];
    4.52  
    4.53 -fun make_conjecture_clauses_aux dfg _ _ [] = []
    4.54 +fun make_conjecture_clauses_aux _ _ _ [] = []
    4.55    | make_conjecture_clauses_aux dfg thy n (th::ths) =
    4.56        make_clause dfg thy (n,"conjecture", RC.Conjecture, th) ::
    4.57        make_conjecture_clauses_aux dfg thy (n+1) ths;
    4.58 @@ -213,9 +213,9 @@
    4.59  fun result_type (RC.Comp ("tc_fun", [_, tp2])) = tp2
    4.60    | result_type _ = error "result_type"
    4.61  
    4.62 -fun type_of_combterm (CombConst(c,tp,_)) = tp
    4.63 -  | type_of_combterm (CombVar(v,tp)) = tp
    4.64 -  | type_of_combterm (CombApp(t1,t2)) = result_type (type_of_combterm t1);
    4.65 +fun type_of_combterm (CombConst (_, tp, _)) = tp
    4.66 +  | type_of_combterm (CombVar (_, tp)) = tp
    4.67 +  | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1);
    4.68  
    4.69  (*gets the head of a combinator application, along with the list of arguments*)
    4.70  fun strip_comb u =
    4.71 @@ -226,7 +226,7 @@
    4.72  val type_wrapper = "ti";
    4.73  
    4.74  fun head_needs_hBOOL const_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL const_needs_hBOOL c
    4.75 -  | head_needs_hBOOL const_needs_hBOOL _ = true;
    4.76 +  | head_needs_hBOOL _ _ = true;
    4.77  
    4.78  fun wrap_type t_full (s, tp) =
    4.79    if t_full then
    4.80 @@ -242,7 +242,7 @@
    4.81  
    4.82  (*Apply an operator to the argument strings, using either the "apply" operator or
    4.83    direct function application.*)
    4.84 -fun string_of_applic t_full cma (CombConst(c,tp,tvars), args) =
    4.85 +fun string_of_applic t_full cma (CombConst (c, _, tvars), args) =
    4.86        let val c = if c = "equal" then "c_fequal" else c
    4.87            val nargs = min_arity_of cma c
    4.88            val args1 = List.take(args, nargs)
    4.89 @@ -255,7 +255,7 @@
    4.90        in
    4.91            string_apply (c ^ RC.paren_pack (args1@targs), args2)
    4.92        end
    4.93 -  | string_of_applic _ cma (CombVar(v,tp), args) = string_apply (v, args)
    4.94 +  | string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args)
    4.95    | string_of_applic _ _ _ = error "string_of_applic";
    4.96  
    4.97  fun wrap_type_if t_full cnh (head, s, tp) =
    4.98 @@ -282,12 +282,6 @@
    4.99                CombConst(c,_,_) => if needs_hBOOL cnh c then boolify params t else string_of_combterm params t
   4.100              | _ => boolify params t;
   4.101  
   4.102 -fun string_of_clausename (cls_id,ax_name) =
   4.103 -    RC.clause_prefix ^ RC.ascii_of ax_name ^ "_" ^ Int.toString cls_id;
   4.104 -
   4.105 -fun string_of_type_clsname (cls_id,ax_name,idx) =
   4.106 -    string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
   4.107 -
   4.108  
   4.109  (*** tptp format ***)
   4.110  
   4.111 @@ -306,7 +300,7 @@
   4.112        (map (tptp_literal params) literals, 
   4.113         map (RC.tptp_of_typeLit pos) (RC.add_typs ctypes_sorts));
   4.114  
   4.115 -fun clause2tptp params (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
   4.116 +fun clause2tptp params (cls as Clause {axiom_name, clause_id, kind, ...}) =
   4.117    let val (lits,tylits) = tptp_type_lits params (kind = RC.Conjecture) cls
   4.118    in
   4.119        (RC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits)
   4.120 @@ -342,7 +336,7 @@
   4.121  
   4.122  fun addtypes tvars tab = List.foldl RC.add_foltype_funcs tab tvars;
   4.123  
   4.124 -fun add_decls (t_full, cma, cnh) (CombConst(c,tp,tvars), (funcs,preds)) =
   4.125 +fun add_decls (t_full, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
   4.126        if c = "equal" then (addtypes tvars funcs, preds)
   4.127        else
   4.128          let val arity = min_arity_of cma c
   4.129 @@ -394,10 +388,10 @@
   4.130                   ("c_COMBB", 0), ("c_COMBC", 0),
   4.131                   ("c_COMBS", 0)];
   4.132  
   4.133 -fun count_combterm (CombConst(c,tp,_), ct) =
   4.134 +fun count_combterm (CombConst (c, _, _), ct) =
   4.135       (case Symtab.lookup ct c of NONE => ct  (*no counter*)
   4.136                                 | SOME n => Symtab.update (c,n+1) ct)
   4.137 -  | count_combterm (CombVar(v,tp), ct) = ct
   4.138 +  | count_combterm (CombVar _, ct) = ct
   4.139    | count_combterm (CombApp(t1,t2), ct) = count_combterm(t1, count_combterm(t2, ct));
   4.140  
   4.141  fun count_literal (Literal(_,t), ct) = count_combterm(t,ct);
   4.142 @@ -448,7 +442,7 @@
   4.143                if toplev then (const_min_arity, const_needs_hBOOL)
   4.144                else (const_min_arity, Symtab.update (a,true) (const_needs_hBOOL))
   4.145              end
   4.146 -        | ts => (const_min_arity, const_needs_hBOOL)
   4.147 +        | _ => (const_min_arity, const_needs_hBOOL)
   4.148    end;
   4.149  
   4.150  (*A literal is a top-level term*)
     5.1 --- a/src/HOL/Tools/res_reconstruct.ML	Sun Oct 18 18:08:04 2009 +0200
     5.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Sun Oct 18 20:53:40 2009 +0200
     5.3 @@ -216,7 +216,7 @@
     5.4          | xs => foldr1 HOLogic.mk_disj (rev xs);
     5.5  
     5.6  (*Accumulate sort constraints in vt, with "real" literals in lits.*)
     5.7 -fun lits_of_strees ctxt (vt, lits) [] = (vt, finish lits)
     5.8 +fun lits_of_strees _ (vt, lits) [] = (vt, finish lits)
     5.9    | lits_of_strees ctxt (vt, lits) (t::ts) =
    5.10        lits_of_strees ctxt (add_constraint (constraint_of_stree true t, vt), lits) ts
    5.11        handle STREE _ =>
    5.12 @@ -303,7 +303,7 @@
    5.13    | match_literal (Free(a1,_)) (Free(a2,_)) env =
    5.14        if a1=a2 then env else raise MATCH_LITERAL
    5.15    | match_literal (Var(ix1,_)) (Var(ix2,_)) env = insert (op =) (ix1,ix2) env
    5.16 -  | match_literal _ _ env = raise MATCH_LITERAL;
    5.17 +  | match_literal _ _ _ = raise MATCH_LITERAL;
    5.18  
    5.19  (*Checking that all variable associations are unique. The list env contains no
    5.20    repetitions, but does it contain say (x,y) and (y,y)? *)
    5.21 @@ -337,7 +337,7 @@
    5.22              then SOME ctm else perm ctms
    5.23    in perm end;
    5.24  
    5.25 -fun have_or_show "show " lname = "show \""
    5.26 +fun have_or_show "show " _ = "show \""
    5.27    | have_or_show have lname = have ^ lname ^ ": \""
    5.28  
    5.29  (*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the
    5.30 @@ -345,7 +345,7 @@
    5.31  fun isar_lines ctxt ctms =
    5.32    let val string_of = PrintMode.setmp [] (fn term => Syntax.string_of_term ctxt term)
    5.33        val _ = trace ("\n\nisar_lines: start\n")
    5.34 -      fun doline have (lname, t, []) =  (*No deps: it's a conjecture clause, with no proof.*)
    5.35 +      fun doline _ (lname, t, []) =  (*No deps: it's a conjecture clause, with no proof.*)
    5.36             (case permuted_clause t ctms of
    5.37                  SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n"
    5.38                | NONE => "assume? " ^ lname ^ ": \"" ^ string_of t ^ "\"\n")  (*no match!!*)
    5.39 @@ -374,17 +374,17 @@
    5.40        else
    5.41         (case take_prefix (notequal t) lines of
    5.42             (_,[]) => lines                  (*no repetition of proof line*)
    5.43 -         | (pre, (lno',t',deps')::post) =>  (*repetition: replace later line by earlier one*)
    5.44 +         | (pre, (lno', _, _) :: post) =>   (*repetition: replace later line by earlier one*)
    5.45               pre @ map (replace_deps (lno', [lno])) post)
    5.46 -  | add_prfline ((lno, role, t, []), lines) =  (*no deps: conjecture clause*)
    5.47 +  | add_prfline ((lno, _, t, []), lines) =  (*no deps: conjecture clause*)
    5.48        (lno, t, []) :: lines
    5.49 -  | add_prfline ((lno, role, t, deps), lines) =
    5.50 +  | add_prfline ((lno, _, t, deps), lines) =
    5.51        if eq_types t then (lno, t, deps) :: lines
    5.52        (*Type information will be deleted later; skip repetition test.*)
    5.53        else (*FIXME: Doesn't this code risk conflating proofs involving different types??*)
    5.54        case take_prefix (notequal t) lines of
    5.55           (_,[]) => (lno, t, deps) :: lines  (*no repetition of proof line*)
    5.56 -       | (pre, (lno',t',deps')::post) =>
    5.57 +       | (pre, (lno', t', _) :: post) =>
    5.58             (lno, t', deps) ::               (*repetition: replace later line by earlier one*)
    5.59             (pre @ map (replace_deps (lno', [lno])) post);
    5.60