# HG changeset patch # User wenzelm # Date 1258710030 -3600 # Node ID e08c9f755fca644fc790dbf2d298bd5f4df8b8ff # Parent b584e0adb4946bcd77bcaf1e940b68704adcbf8a# Parent 6d8630fab26a3075b8fd8350d498f91991145d66 merged diff -r b584e0adb494 -r e08c9f755fca src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Fri Nov 20 09:22:14 2009 +0100 +++ b/src/HOL/Nominal/nominal_primrec.ML Fri Nov 20 10:40:30 2009 +0100 @@ -280,7 +280,7 @@ else primrec_err ("functions " ^ commas_quote names2 ^ "\nare not mutually recursive"); val (defs_thms, lthy') = lthy |> - fold_map (apfst (snd o snd) oo Local_Theory.define Thm.definitionK o fst) defs'; + fold_map (apfst (snd o snd) oo Local_Theory.define o fst) defs'; val qualify = Binding.qualify false (space_implode "_" (map (Long_Name.base_name o #1) defs)); val names_atts' = map (apfst qualify) names_atts; diff -r b584e0adb494 -r e08c9f755fca src/HOL/Tools/Function/function_core.ML --- a/src/HOL/Tools/Function/function_core.ML Fri Nov 20 09:22:14 2009 +0100 +++ b/src/HOL/Tools/Function/function_core.ML Fri Nov 20 10:40:30 2009 +0100 @@ -518,7 +518,7 @@ $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0)) |> Syntax.check_term lthy in - Local_Theory.define "" + Local_Theory.define ((Binding.name (function_name fname), mixfix), ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy end diff -r b584e0adb494 -r e08c9f755fca src/HOL/Tools/Function/mutual.ML --- a/src/HOL/Tools/Function/mutual.ML Fri Nov 20 09:22:14 2009 +0100 +++ b/src/HOL/Tools/Function/mutual.ML Fri Nov 20 10:40:30 2009 +0100 @@ -146,7 +146,7 @@ fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy = let val ((f, (_, f_defthm)), lthy') = - Local_Theory.define "" + Local_Theory.define ((Binding.name fname, mixfix), ((Binding.conceal (Binding.name (fname ^ "_def")), []), Term.subst_bound (fsum, f_def))) lthy diff -r b584e0adb494 -r e08c9f755fca src/HOL/Tools/Function/size.ML --- a/src/HOL/Tools/Function/size.ML Fri Nov 20 09:22:14 2009 +0100 +++ b/src/HOL/Tools/Function/size.ML Fri Nov 20 10:40:30 2009 +0100 @@ -130,8 +130,8 @@ fun define_overloaded (def_name, eq) lthy = let val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq; - val ((_, (_, thm)), lthy') = lthy |> Local_Theory.define Thm.definitionK - ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs)); + val ((_, (_, thm)), lthy') = lthy + |> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs)); val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy'); val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm; in (thm', lthy') end; diff -r b584e0adb494 -r e08c9f755fca src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Fri Nov 20 09:22:14 2009 +0100 +++ b/src/HOL/Tools/inductive.ML Fri Nov 20 10:40:30 2009 +0100 @@ -666,7 +666,7 @@ val ((rec_const, (_, fp_def)), lthy') = lthy |> Local_Theory.conceal - |> Local_Theory.define "" + |> Local_Theory.define ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn), ((Binding.empty, [Attrib.internal (K Nitpick_Defs.add)]), fold_rev lambda params @@ -689,7 +689,7 @@ end) (cnames_syn ~~ cs); val (consts_defs, lthy'') = lthy' |> Local_Theory.conceal - |> fold_map (Local_Theory.define "") specs + |> fold_map Local_Theory.define specs ||> Local_Theory.restore_naming lthy'; val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs); diff -r b584e0adb494 -r e08c9f755fca src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Fri Nov 20 09:22:14 2009 +0100 +++ b/src/HOL/Tools/inductive_set.ML Fri Nov 20 10:40:30 2009 +0100 @@ -485,7 +485,7 @@ (* define inductive sets using previously defined predicates *) val (defs, lthy2) = lthy1 |> Local_Theory.conceal (* FIXME ?? *) - |> fold_map (Local_Theory.define "") + |> fold_map Local_Theory.define (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding, fold_rev lambda params (HOLogic.Collect_const U $ HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3)))))) diff -r b584e0adb494 -r e08c9f755fca src/HOL/Tools/primrec.ML --- a/src/HOL/Tools/primrec.ML Fri Nov 20 09:22:14 2009 +0100 +++ b/src/HOL/Tools/primrec.ML Fri Nov 20 10:40:30 2009 +0100 @@ -259,7 +259,7 @@ val ((prefix, (fs, defs)), prove) = distill lthy fixes ts; in lthy - |> fold_map (Local_Theory.define Thm.definitionK) defs + |> fold_map Local_Theory.define defs |-> (fn defs => `(fn lthy => (prefix, prove lthy defs))) end; diff -r b584e0adb494 -r e08c9f755fca src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Fri Nov 20 09:22:14 2009 +0100 +++ b/src/HOL/Tools/quickcheck_generators.ML Fri Nov 20 10:40:30 2009 +0100 @@ -190,7 +190,7 @@ in lthy |> random_aux_primrec aux_eq' - ||>> fold_map (Local_Theory.define Thm.definitionK) proj_defs + ||>> fold_map Local_Theory.define proj_defs |-> (fn (aux_simp, proj_defs) => prove_eqs aux_simp proj_defs) end; diff -r b584e0adb494 -r e08c9f755fca src/HOLCF/Tools/fixrec.ML --- a/src/HOLCF/Tools/fixrec.ML Fri Nov 20 09:22:14 2009 +0100 +++ b/src/HOLCF/Tools/fixrec.ML Fri Nov 20 10:40:30 2009 +0100 @@ -209,9 +209,8 @@ | defs (l::[]) r = [one_def l r] | defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r); val fixdefs = defs lhss fixpoint; - val define_all = fold_map (Local_Theory.define Thm.definitionK); val (fixdef_thms : (term * (string * thm)) list, lthy') = lthy - |> define_all (map (apfst fst) fixes ~~ fixdefs); + |> fold_map Local_Theory.define (map (apfst fst) fixes ~~ fixdefs); fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2]; val tuple_fixdef_thm = foldr1 pair_equalI (map (snd o snd) fixdef_thms); val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT); diff -r b584e0adb494 -r e08c9f755fca src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Fri Nov 20 09:22:14 2009 +0100 +++ b/src/Pure/Isar/local_theory.ML Fri Nov 20 10:40:30 2009 +0100 @@ -32,7 +32,7 @@ val pretty: local_theory -> Pretty.T list val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory - val define: string -> (binding * mixfix) * (Attrib.binding * term) -> local_theory -> + val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory -> (term * (string * thm)) * local_theory val note: Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory val notes: (Attrib.binding * (thm list * Attrib.src list) list) list -> @@ -63,8 +63,7 @@ {pretty: local_theory -> Pretty.T list, abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory, - define: string -> - (binding * mixfix) * (Attrib.binding * term) -> local_theory -> + define: (binding * mixfix) * (Attrib.binding * term) -> local_theory -> (term * (string * thm)) * local_theory, notes: string -> (Attrib.binding * (thm list * Attrib.src list) list) list -> @@ -185,11 +184,12 @@ (* basic operations *) fun operation f lthy = f (#operations (get_lthy lthy)) lthy; +fun operation1 f x = operation (fn ops => f ops x); fun operation2 f x y lthy = operation (fn ops => f ops x y) lthy; val pretty = operation #pretty; val abbrev = apsnd checkpoint ooo operation2 #abbrev; -val define = apsnd checkpoint ooo operation2 #define; +val define = apsnd checkpoint oo operation1 #define; val notes_kind = apsnd checkpoint ooo operation2 #notes; val type_syntax = checkpoint ooo operation2 #type_syntax; val term_syntax = checkpoint ooo operation2 #term_syntax; diff -r b584e0adb494 -r e08c9f755fca src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Fri Nov 20 09:22:14 2009 +0100 +++ b/src/Pure/Isar/specification.ML Fri Nov 20 10:40:30 2009 +0100 @@ -204,8 +204,7 @@ in (b, mx) end); val name = Thm.def_binding_optional b raw_name; val ((lhs, (_, raw_th)), lthy2) = lthy - |> Local_Theory.define Thm.definitionK - (var, ((Binding.suffix_name "_raw" name, []), rhs)); + |> Local_Theory.define (var, ((Binding.suffix_name "_raw" name, []), rhs)); val th = prove lthy2 raw_th; val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]); diff -r b584e0adb494 -r e08c9f755fca src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Fri Nov 20 09:22:14 2009 +0100 +++ b/src/Pure/Isar/theory_target.ML Fri Nov 20 10:40:30 2009 +0100 @@ -270,7 +270,7 @@ (* define *) -fun define ta kind ((b, mx), ((name, atts), rhs)) lthy = +fun define ta ((b, mx), ((name, atts), rhs)) lthy = let val thy = ProofContext.theory_of lthy; val thy_ctxt = ProofContext.init thy; @@ -301,7 +301,7 @@ (*note*) val ([(res_name, [res])], lthy4) = lthy3 - |> notes ta kind [((name', atts), [([def], [])])]; + |> notes ta "" [((name', atts), [([def], [])])]; in ((lhs, (res_name, res)), lthy4) end; diff -r b584e0adb494 -r e08c9f755fca src/Pure/ML-Systems/install_pp_polyml-5.3.ML --- a/src/Pure/ML-Systems/install_pp_polyml-5.3.ML Fri Nov 20 09:22:14 2009 +0100 +++ b/src/Pure/ML-Systems/install_pp_polyml-5.3.ML Fri Nov 20 10:40:30 2009 +0100 @@ -3,6 +3,9 @@ Extra toplevel pretty-printing for Poly/ML 5.3.0. *) +PolyML.addPrettyPrinter (fn depth => fn pretty => fn var => + pretty (Synchronized.value var, depth)); + PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => (case Future.peek x of NONE => PolyML.PrettyString "" diff -r b584e0adb494 -r e08c9f755fca src/Pure/Thy/thm_deps.ML --- a/src/Pure/Thy/thm_deps.ML Fri Nov 20 09:22:14 2009 +0100 +++ b/src/Pure/Thy/thm_deps.ML Fri Nov 20 10:40:30 2009 +0100 @@ -59,17 +59,17 @@ end; fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts; - val thms = + val new_thms = fold (add_facts o PureThy.facts_of) thys [] |> sort_distinct (string_ord o pairself #1); - val tab = + val used = Proofterm.fold_body_thms (fn (a, prop, _) => a <> "" ? Symtab.insert_list (op =) (a, prop)) - (map (Proofterm.strip_thm o Thm.proof_body_of o #1 o #2) thms) Symtab.empty; + (map (Proofterm.strip_thm o Thm.proof_body_of o #1 o #2) new_thms) Symtab.empty; fun is_unused (a, th) = - not (member (op aconv) (Symtab.lookup_list tab a) (Thm.prop_of th)); + not (member (op aconv) (Symtab.lookup_list used a) (Thm.prop_of th)); (* groups containing at least one used theorem *) val used_groups = fold (fn (a, (th, _, group)) => @@ -77,18 +77,20 @@ else (case group of NONE => I - | SOME grp => Inttab.update (grp, ()))) thms Inttab.empty; - val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, grps') => - if not concealed andalso is_unused (a, th) then + | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty; + + val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) => + if not concealed andalso + member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK] (Thm.get_kind th) andalso + is_unused (a, th) + then (case group of - NONE => ((a, th) :: thms, grps') + NONE => ((a, th) :: thms, seen_groups) | SOME grp => - (* do not output theorem if another theorem in group has been used *) - if Inttab.defined used_groups grp then q - (* output at most one unused theorem per group *) - else if Inttab.defined grps' grp then q - else ((a, th) :: thms, Inttab.update (grp, ()) grps')) - else q) thms ([], Inttab.empty) + if Inttab.defined used_groups grp orelse + Inttab.defined seen_groups grp then q + else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups)) + else q) new_thms ([], Inttab.empty); in rev thms' end; end; diff -r b584e0adb494 -r e08c9f755fca src/Pure/goal.ML --- a/src/Pure/goal.ML Fri Nov 20 09:22:14 2009 +0100 +++ b/src/Pure/goal.ML Fri Nov 20 10:40:30 2009 +0100 @@ -132,7 +132,8 @@ cert (Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop)))) |> Thm.weaken_sorts (Variable.sorts_of ctxt); val global_result = result |> Future.map - (Thm.adjust_maxidx_thm ~1 #> + (Drule.flexflex_unique #> + Thm.adjust_maxidx_thm ~1 #> Drule.implies_intr_list assms #> Drule.forall_intr_list fixes #> Thm.generalize (map #1 tfrees, []) 0);