# HG changeset patch # User wenzelm # Date 1257438975 -3600 # Node ID 64205e046dcab1c969ce4f31d875342b28565aa9 # Parent 5d78b2bd27dee8a50a614ebf0469642bb4be09f9# Parent 4389ec600ba7455e5afa502aef38fcd80fd2189a merged diff -r 4389ec600ba7 -r 64205e046dca src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Nov 05 16:23:51 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Nov 05 17:36:15 2009 +0100 @@ -546,9 +546,9 @@ val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT)) val elim_t = Logic.list_implies ([clausehd, Logic.mk_implies (@{prop False}, P)], P) val intro = Goal.prove (ProofContext.init thy) names [] intro_t - (fn {...} => etac @{thm FalseE} 1) + (fn _ => etac @{thm FalseE} 1) val elim = Goal.prove (ProofContext.init thy) ("P" :: names) [] elim_t - (fn {...} => etac elim 1) + (fn _ => etac elim 1) in ([intro], elim) end @@ -1440,10 +1440,14 @@ val simprules = [defthm, @{thm eval_pred}, @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}] val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1 - val introthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y"]) [] introtrm (fn {...} => unfolddef_tac) + val introthm = + Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y"]) [] introtrm + (fn _ => unfolddef_tac) val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT)); val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P) - val elimthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y", "P"]) [] elimtrm (fn {...} => unfolddef_tac) + val elimthm = + Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y", "P"]) [] elimtrm + (fn _ => unfolddef_tac) in (introthm, elimthm) end; @@ -2157,7 +2161,7 @@ val eq_term = HOLogic.mk_Trueprop (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs)) val def = predfun_definition_of thy predname full_mode - val tac = fn {...} => Simplifier.simp_tac + val tac = fn _ => Simplifier.simp_tac (HOL_basic_ss addsimps [def, @{thm eval_pred}]) 1 val eq = Goal.prove (ProofContext.init thy) arg_names [] eq_term tac in diff -r 4389ec600ba7 -r 64205e046dca src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Nov 05 16:23:51 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Nov 05 17:36:15 2009 +0100 @@ -113,7 +113,7 @@ val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt val t' = Pattern.rewrite_term thy rewr [] t val tac = Skip_Proof.cheat_tac thy - val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn {...} => tac) + val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn _ => tac) val th''' = LocalDefs.unfold ctxt [@{thm split_conv}] th'' in th''' diff -r 4389ec600ba7 -r 64205e046dca src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Nov 05 16:23:51 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Nov 05 17:36:15 2009 +0100 @@ -98,7 +98,7 @@ THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN atac 1) THEN TRY (atac 1) in - Goal.prove ctxt' (map fst ps) [] introrule (fn {...} => tac) + Goal.prove ctxt' (map fst ps) [] introrule (fn _ => tac) end in map_index prove_introrule (map mk_introrule disjuncts) diff -r 4389ec600ba7 -r 64205e046dca src/HOLCF/Tools/adm_tac.ML --- a/src/HOLCF/Tools/adm_tac.ML Thu Nov 05 16:23:51 2009 +0100 +++ b/src/HOLCF/Tools/adm_tac.ML Thu Nov 05 17:36:15 2009 +0100 @@ -1,4 +1,5 @@ -(* Author: Stefan Berghofer, TU Muenchen +(* Title: HOLCF/Tools/adm_tac.ML + Author: Stefan Berghofer, TU Muenchen Admissibility tactic. @@ -18,7 +19,7 @@ val adm_tac: Proof.context -> (int -> tactic) -> int -> tactic end; -structure Adm :> ADM = +structure Adm : ADM = struct diff -r 4389ec600ba7 -r 64205e046dca src/HOLCF/Tools/fixrec.ML --- a/src/HOLCF/Tools/fixrec.ML Thu Nov 05 16:23:51 2009 +0100 +++ b/src/HOLCF/Tools/fixrec.ML Thu Nov 05 17:36:15 2009 +0100 @@ -13,8 +13,8 @@ val add_fixpat: Thm.binding * term list -> theory -> theory val add_fixpat_cmd: Attrib.binding * string list -> theory -> theory val add_matchers: (string * string) list -> theory -> theory - val fixrec_simp_add: Thm.attribute - val fixrec_simp_del: Thm.attribute + val fixrec_simp_add: attribute + val fixrec_simp_del: attribute val fixrec_simp_tac: Proof.context -> int -> tactic val setup: theory -> theory end; @@ -165,7 +165,7 @@ val empty = Symtab.empty; val copy = I; val extend = I; - val merge = K (Symtab.merge (K true)); + fun merge _ = Symtab.merge (K true); ); local @@ -179,7 +179,7 @@ in -val add_unfold : Thm.attribute = +val add_unfold : attribute = Thm.declaration_attribute (fn th => FixrecUnfoldData.map (Symtab.insert (K true) (lhs_name th, th))); @@ -257,7 +257,7 @@ val empty = Symtab.empty; val copy = I; val extend = I; - val merge = K (Symtab.merge (K true)); + fun merge _ = Symtab.merge (K true); ); (* associate match functions with pattern constants *) @@ -372,7 +372,7 @@ addsimprocs [@{simproc cont_proc}]; val copy = I; val extend = I; - val merge = K merge_ss; + fun merge _ = merge_ss; ); fun fixrec_simp_tac ctxt = @@ -391,14 +391,14 @@ CHANGED (rtac rule i THEN asm_simp_tac ss i) end in - SUBGOAL (fn ti => tac ti handle _ => no_tac) + SUBGOAL (fn ti => tac ti handle _ => no_tac) (* FIXME avoid handle _ *) end; -val fixrec_simp_add : Thm.attribute = +val fixrec_simp_add : attribute = Thm.declaration_attribute (fn th => FixrecSimpData.map (fn ss => ss addsimps [th])); -val fixrec_simp_del : Thm.attribute = +val fixrec_simp_del : attribute = Thm.declaration_attribute (fn th => FixrecSimpData.map (fn ss => ss delsimps [th]));