--- 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;
--- 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
--- 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
--- 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;
--- 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);
--- 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))))))
--- 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;
--- 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;
--- 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);
--- 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;
--- 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]);
--- 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;
--- 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 "<future>"
--- 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;
--- 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);