--- a/NEWS Wed Jun 22 16:04:03 2016 +0200
+++ b/NEWS Thu Jun 23 11:01:14 2016 +0200
@@ -478,6 +478,9 @@
relatively to the master directory of a theory (see also
File.full_path). Potential INCOMPATIBILITY.
+* Binding.empty_atts supersedes Thm.empty_binding and
+Attrib.empty_binding. Minor INCOMPATIBILITY.
+
*** System ***
--- a/src/HOL/HOLCF/Tools/fixrec.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Thu Jun 23 11:01:14 2016 +0200
@@ -356,7 +356,7 @@
| NONE => fixrec_err ("unknown pattern constructor: " ^ c)
val matches = map (compile_eqs match_name) (map (map (snd o fst)) blocks)
- val spec' = map (pair Attrib.empty_binding) matches
+ val spec' = map (pair Binding.empty_atts) matches
val (lthy, _, _, unfold_thms) =
add_fixdefs fixes spec' lthy
@@ -388,7 +388,7 @@
(*************************************************************************)
val opt_thm_name' : (bool * Attrib.binding) parser =
- @{keyword "("} -- @{keyword "unchecked"} -- @{keyword ")"} >> K (true, Attrib.empty_binding)
+ @{keyword "("} -- @{keyword "unchecked"} -- @{keyword ")"} >> K (true, Binding.empty_atts)
|| Parse_Spec.opt_thm_name ":" >> pair false
val spec' : (bool * (Attrib.binding * string)) parser =
--- a/src/HOL/Library/simps_case_conv.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Library/simps_case_conv.ML Thu Jun 23 11:01:14 2016 +0200
@@ -137,7 +137,7 @@
val frees = fold Term.add_frees pat []
val abs_rhs = fold absfree frees rhs
val ([(f, (_, def))], lthy') = lthy
- |> Local_Defs.define [((Binding.name name, NoSyn), (Thm.empty_binding, abs_rhs))]
+ |> Local_Defs.define [((Binding.name name, NoSyn), (Binding.empty_atts, abs_rhs))]
in ((list_comb (f, map Free (rev frees)), def), lthy') end
val ((def_ts, def_thms), ctxt2) =
--- a/src/HOL/Nominal/nominal_atoms.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Thu Jun 23 11:01:14 2016 +0200
@@ -192,7 +192,7 @@
thy' |>
BNF_LFP_Compat.primrec_global
[(Binding.name swap_name, SOME swapT, NoSyn)]
- [((Attrib.empty_binding, def1), [], [])] ||>
+ [((Binding.empty_atts, def1), [], [])] ||>
Sign.parent_path ||>>
Global_Theory.add_defs_unchecked true
[((Binding.name name, def2), [])] |>> (snd o fst)
@@ -226,7 +226,7 @@
thy' |>
BNF_LFP_Compat.primrec_global
[(Binding.name prm_name, SOME prmT, NoSyn)]
- (map (fn def => ((Attrib.empty_binding, def), [], [])) [def1, def2]) ||>
+ (map (fn def => ((Binding.empty_atts, def), [], [])) [def1, def2]) ||>
Sign.parent_path
end) ak_names_types thy3;
--- a/src/HOL/Nominal/nominal_datatype.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Thu Jun 23 11:01:14 2016 +0200
@@ -251,7 +251,7 @@
else Const (@{const_name Nominal.perm}, permT --> T --> T) $ pi $ x
end;
in
- ((Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
+ ((Binding.empty_atts, HOLogic.mk_Trueprop (HOLogic.mk_eq
(Free (nth perm_names_types' i) $
Free ("pi", mk_permT (TFree ("'x", @{sort type}))) $
list_comb (c, args),
@@ -544,7 +544,7 @@
coind = false, no_elim = true, no_ind = false, skip_mono = true}
(map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
(rep_set_names' ~~ recTs'))
- [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
+ [] (map (fn x => (Binding.empty_atts, x)) intr_ts) []
||> Sign.restore_naming thy3;
(**** Prove that representing set is closed under permutation ****)
@@ -1533,7 +1533,7 @@
coind = false, no_elim = false, no_ind = false, skip_mono = true}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
- (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
+ (map (fn x => (Binding.empty_atts, x)) rec_intr_ts) []
||> Global_Theory.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct")
||> Sign.restore_naming thy10;
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Thu Jun 23 11:01:14 2016 +0200
@@ -795,7 +795,7 @@
((Binding.name ("H" ^ s'), []), [(prop_of e, [])])) ps),
Element.Shows (map (fn (s', e) =>
(if name_concl then (Binding.name ("C" ^ s'), [])
- else Attrib.empty_binding,
+ else Binding.empty_atts,
[(prop_of e, mk_pat s')])) cs))
end;
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Thu Jun 23 11:01:14 2016 +0200
@@ -265,7 +265,7 @@
val (([free], [def_free], [simps_free]), (lthy, lthy_old)) = lthy
|> Local_Theory.open_target |> snd
|> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*)
- |> primrec [(b, NONE, NoSyn)] (map (fn eq => ((Attrib.empty_binding, eq), [], [])) eqs)
+ |> primrec [(b, NONE, NoSyn)] (map (fn eq => ((Binding.empty_atts, eq), [], [])) eqs)
||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Thu Jun 23 11:01:14 2016 +0200
@@ -285,7 +285,7 @@
handle Fail _ => [];
fun set_transfer_rule_attrs thms =
- snd o Local_Theory.notes [((Binding.empty, []), [(thms, transfer_rule_attrs)])];
+ snd o Local_Theory.notes [(Binding.empty_atts, [(thms, transfer_rule_attrs)])];
fun ensure_codatatype_extra fpT_name ctxt =
(case codatatype_extra_of ctxt fpT_name of
@@ -1995,7 +1995,7 @@
val (plugins, friend, transfer) = get_options lthy opts;
val ([((b, fun_T), mx)], [(_, eq)]) =
- fst (Specification.read_multi_specs raw_fixes [((Attrib.empty_binding, raw_eq), [], [])] lthy);
+ fst (Specification.read_multi_specs raw_fixes [((Binding.empty_atts, raw_eq), [], [])] lthy);
val _ = Sign.of_sort (Proof_Context.theory_of lthy) (fun_T, @{sort type}) orelse
error ("Type of " ^ Binding.print b ^ " contains top sort");
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Jun 23 11:01:14 2016 +0200
@@ -1609,7 +1609,7 @@
|| Parse.reserved "transfer" >> K Transfer_Option);
val where_alt_props_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|"
- ((Parse.prop >> pair Attrib.empty_binding) -- Scan.option (Parse.reserved "of" |-- Parse.const)));
+ ((Parse.prop >> pair Binding.empty_atts) -- Scan.option (Parse.reserved "of" |-- Parse.const)));
val _ = Outer_Syntax.local_theory_to_proof @{command_keyword primcorecursive}
"define primitive corecursive functions"
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Thu Jun 23 11:01:14 2016 +0200
@@ -93,7 +93,7 @@
mk_Trueprop_eq (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq})
|> Syntax.check_term lthy;
val ((_, (_, raw_def)), lthy') =
- Specification.definition NONE [] [] (Attrib.empty_binding, spec) lthy;
+ Specification.definition NONE [] [] (Binding.empty_atts, spec) lthy;
val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy');
val def = singleton (Proof_Context.export lthy' thy_ctxt) raw_def;
in
--- a/src/HOL/Tools/Function/fun.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Tools/Function/fun.ML Thu Jun 23 11:01:14 2016 +0200
@@ -134,7 +134,7 @@
|> map (map snd)
- val bnds' = bnds @ replicate (length spliteqs - length bnds) Attrib.empty_binding
+ val bnds' = bnds @ replicate (length spliteqs - length bnds) Binding.empty_atts
(* using theorem names for case name currently disabled *)
val case_names = map_index (fn (i, (_, es)) => mk_case_names i "" (length es))
--- a/src/HOL/Tools/Function/function_core.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Thu Jun 23 11:01:14 2016 +0200
@@ -450,7 +450,7 @@
skip_mono = true}
[binding] (* relation *)
[] (* no parameters *)
- (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
+ (map (fn t => (Binding.empty_atts, t)) intrs) (* intro rules *)
[] (* no special monos *)
||> Proof_Context.restore_naming lthy
--- a/src/HOL/Tools/Lifting/lifting_bnf.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Thu Jun 23 11:01:14 2016 +0200
@@ -82,17 +82,17 @@
(* relator_eq_onp *)
fun relator_eq_onp bnf =
- [((Binding.empty, []), [([rel_eq_onp_of_bnf bnf], @{attributes [relator_eq_onp]})])]
+ [(Binding.empty_atts, [([rel_eq_onp_of_bnf bnf], @{attributes [relator_eq_onp]})])]
(* relator_mono *)
fun relator_mono bnf =
- [((Binding.empty, []), [([rel_mono_of_bnf bnf], @{attributes [relator_mono]})])]
+ [(Binding.empty_atts, [([rel_mono_of_bnf bnf], @{attributes [relator_mono]})])]
(* relator_distr *)
fun relator_distr bnf =
- [((Binding.empty, []), [([rel_OO_of_bnf bnf RS sym], @{attributes [relator_distr]})])]
+ [(Binding.empty_atts, [([rel_OO_of_bnf bnf RS sym], @{attributes [relator_distr]})])]
(* interpretation *)
--- a/src/HOL/Tools/Lifting/lifting_def.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Thu Jun 23 11:01:14 2016 +0200
@@ -29,24 +29,24 @@
val generate_parametric_transfer_rule:
Proof.context -> thm -> thm -> thm
- val add_lift_def:
- config -> binding * mixfix -> typ -> term -> thm -> thm list -> local_theory ->
+ val add_lift_def:
+ config -> binding * mixfix -> typ -> term -> thm -> thm list -> local_theory ->
lift_def * local_theory
-
+
val prepare_lift_def:
- (binding * mixfix -> typ -> term -> thm -> thm list -> Proof.context ->
- lift_def * local_theory) ->
- binding * mixfix -> typ -> term -> thm list -> local_theory ->
+ (binding * mixfix -> typ -> term -> thm -> thm list -> Proof.context ->
+ lift_def * local_theory) ->
+ binding * mixfix -> typ -> term -> thm list -> local_theory ->
term option * (thm -> Proof.context -> lift_def * local_theory)
val gen_lift_def:
- (binding * mixfix -> typ -> term -> thm -> thm list -> local_theory ->
- lift_def * local_theory) ->
- binding * mixfix -> typ -> term -> (Proof.context -> tactic) -> thm list ->
+ (binding * mixfix -> typ -> term -> thm -> thm list -> local_theory ->
+ lift_def * local_theory) ->
+ binding * mixfix -> typ -> term -> (Proof.context -> tactic) -> thm list ->
local_theory -> lift_def * local_theory
- val lift_def:
- config -> binding * mixfix -> typ -> term -> (Proof.context -> tactic) -> thm list ->
+ val lift_def:
+ config -> binding * mixfix -> typ -> term -> (Proof.context -> tactic) -> thm list ->
local_theory -> lift_def * local_theory
val can_generate_code_cert: thm -> bool
@@ -89,7 +89,7 @@
fun mk_lift_def rty qty rhs lift_const def_thm rsp_thm abs_eq rep_eq code_eq transfer_rules =
LIFT_DEF {rty = rty, qty = qty,
rhs = rhs, lift_const = lift_const,
- def_thm = def_thm, rsp_thm = rsp_thm, abs_eq = abs_eq, rep_eq = rep_eq,
+ def_thm = def_thm, rsp_thm = rsp_thm, abs_eq = abs_eq, rep_eq = rep_eq,
code_eq = code_eq, transfer_rules = transfer_rules };
fun map_lift_def f1 f2 f3 f4 f5 f6 f7 f8 f9 f10
@@ -129,8 +129,8 @@
let
val refl_rules = Lifting_Info.get_reflexivity_rules ctxt
val transfer_rules = Transfer.get_transfer_raw ctxt
-
- fun main_tac i = (REPEAT_ALL_NEW (DETERM o resolve_tac ctxt refl_rules) THEN_ALL_NEW
+
+ fun main_tac i = (REPEAT_ALL_NEW (DETERM o resolve_tac ctxt refl_rules) THEN_ALL_NEW
(REPEAT_ALL_NEW (DETERM o resolve_tac ctxt transfer_rules))) i
in
SOME (Goal.prove ctxt [] [] prop (K (main_tac 1)))
@@ -143,7 +143,7 @@
let
val T = fastype_of x
in
- Const (@{const_name "less_eq"}, T --> T --> HOLogic.boolT) $
+ Const (@{const_name "less_eq"}, T --> T --> HOLogic.boolT) $
(Const (@{const_name HOL.eq}, T)) $ x
end;
val goal = HOLogic.mk_Trueprop (mk_ge_eq rel);
@@ -165,11 +165,11 @@
| NONE => NONE
end
-(*
+(*
Generates a parametrized transfer rule.
transfer_rule - of the form T t f
parametric_transfer_rule - of the form par_R t' t
-
+
Result: par_T t' f, after substituing op= for relations in par_R that relate
a type constructor to the same type constructor, it is a merge of (par_R' OO T) t' f
using Lifting_Term.merge_transfer_relations
@@ -182,8 +182,8 @@
val tm = (strip_args 2 o HOLogic.dest_Trueprop o Thm.concl_of) thm;
val param_rel = (snd o dest_comb o fst o dest_comb) tm;
val free_vars = Term.add_vars param_rel [];
-
- fun make_subst (xi, typ) subst =
+
+ fun make_subst (xi, typ) subst =
let
val [rty, rty'] = binder_types typ
in
@@ -195,7 +195,7 @@
val inst_thm = infer_instantiate ctxt (fold make_subst free_vars []) thm;
in
- Conv.fconv_rule
+ Conv.fconv_rule
((Conv.concl_conv (Thm.nprems_of inst_thm) o
HOLogic.Trueprop_conv o Conv.fun2_conv o Conv.arg1_conv)
(Raw_Simplifier.rewrite ctxt false (Transfer.get_sym_relator_eq ctxt))) inst_thm
@@ -227,7 +227,7 @@
in
[Lifting_Term.merge_transfer_relations ctxt goal, thm] MRSL @{thm POS_apply}
end
-
+
val thm =
inst_relcomppI ctxt parametric_transfer_rule transfer_rule
OF [parametric_transfer_rule, transfer_rule]
@@ -248,9 +248,9 @@
zipped_thm
end
-fun print_generate_transfer_info msg =
+fun print_generate_transfer_info msg =
let
- val error_msg = cat_lines
+ val error_msg = cat_lines
["Generation of a parametric transfer rule failed.",
(Pretty.string_of (Pretty.block
[Pretty.str "Reason:", Pretty.brk 2, msg]))]
@@ -279,18 +279,18 @@
fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W)
| get_binder_types _ = []
-fun get_binder_types_by_rel (Const (@{const_name "rel_fun"}, _) $ _ $ S) (Type ("fun", [T, U]), Type ("fun", [V, W])) =
+fun get_binder_types_by_rel (Const (@{const_name "rel_fun"}, _) $ _ $ S) (Type ("fun", [T, U]), Type ("fun", [V, W])) =
(T, V) :: get_binder_types_by_rel S (U, W)
| get_binder_types_by_rel _ _ = []
-fun get_body_type_by_rel (Const (@{const_name "rel_fun"}, _) $ _ $ S) (Type ("fun", [_, U]), Type ("fun", [_, V])) =
+fun get_body_type_by_rel (Const (@{const_name "rel_fun"}, _) $ _ $ S) (Type ("fun", [_, U]), Type ("fun", [_, V])) =
get_body_type_by_rel S (U, V)
| get_body_type_by_rel _ (U, V) = (U, V)
fun get_binder_rels (Const (@{const_name "rel_fun"}, _) $ R $ S) = R :: get_binder_rels S
| get_binder_rels _ = []
-fun force_rty_type ctxt rty rhs =
+fun force_rty_type ctxt rty rhs =
let
val thy = Proof_Context.theory_of ctxt
val rhs_schematic = singleton (Variable.polymorphic ctxt) rhs
@@ -300,7 +300,7 @@
Envir.subst_term_types match rhs_schematic
end
-fun unabs_def ctxt def =
+fun unabs_def ctxt def =
let
val (_, rhs) = Thm.dest_equals (Thm.cprop_of def)
fun dest_abs (Abs (var_name, T, _)) = (var_name, T)
@@ -313,15 +313,15 @@
singleton (Proof_Context.export ctxt' ctxt)
end
-fun unabs_all_def ctxt def =
+fun unabs_all_def ctxt def =
let
val (_, rhs) = Thm.dest_equals (Thm.cprop_of def)
val xs = strip_abs_vars (Thm.term_of rhs)
- in
+ in
fold (K (unabs_def ctxt)) xs def
end
-val map_fun_unfolded =
+val map_fun_unfolded =
@{thm map_fun_def[abs_def]} |>
unabs_def @{context} |>
unabs_def @{context} |>
@@ -331,7 +331,7 @@
let
fun unfold_conv ctm =
case (Thm.term_of ctm) of
- Const (@{const_name "map_fun"}, _) $ _ $ _ =>
+ Const (@{const_name "map_fun"}, _) $ _ $ _ =>
(Conv.arg_conv unfold_conv then_conv Conv.rewr_conv map_fun_unfolded) ctm
| _ => Conv.all_conv ctm
in
@@ -340,14 +340,14 @@
fun unfold_fun_maps_beta ctm =
let val try_beta_conv = Conv.try_conv (Thm.beta_conversion false)
- in
- (unfold_fun_maps then_conv try_beta_conv) ctm
+ in
+ (unfold_fun_maps then_conv try_beta_conv) ctm
end
fun prove_rel ctxt rsp_thm (rty, qty) =
let
val ty_args = get_binder_types (rty, qty)
- fun disch_arg args_ty thm =
+ fun disch_arg args_ty thm =
let
val quot_thm = Lifting_Term.prove_quot_thm ctxt args_ty
in
@@ -359,7 +359,7 @@
exception CODE_CERT_GEN of string
-fun simplify_code_eq ctxt def_thm =
+fun simplify_code_eq ctxt def_thm =
Local_Defs.unfold0 ctxt [@{thm o_apply}, @{thm map_fun_def}, @{thm id_apply}] def_thm
(*
@@ -378,10 +378,10 @@
let
val unfolded_def = Conv.fconv_rule (Conv.arg_conv unfold_fun_maps_beta) def_thm
val unabs_def = unabs_all_def ctxt unfolded_def
- in
- if body_type rty = body_type qty then
+ in
+ if body_type rty = body_type qty then
SOME (simplify_code_eq ctxt (unabs_def RS @{thm meta_eq_to_obj_eq}))
- else
+ else
let
val quot_thm = Lifting_Term.prove_quot_thm ctxt (get_body_types (rty, qty))
val rel_fun = prove_rel ctxt rsp_thm (rty, qty)
@@ -411,8 +411,8 @@
val ty_args = get_binder_types_by_rel rel (rty, qty)
val body_type = get_body_type_by_rel rel (rty, qty)
val quot_ret_thm = Lifting_Term.prove_quot_thm ctxt body_type
-
- val rep_abs_folded_unmapped_thm =
+
+ val rep_abs_folded_unmapped_thm =
let
val rep_id = [quot_thm, def_thm] MRSL @{thm Quotient_Rep_eq}
val ctm = Thm.dest_equals_lhs (Thm.cprop_of rep_id)
@@ -428,10 +428,10 @@
|> fold (fn _ => fn thm => thm RS @{thm rel_funD2}) ty_args
|> (fn x => x RS (@{thm Quotient_rel_abs2} OF [quot_ret_thm]))
end
-
+
val prem_rels = get_binder_rels (quot_thm_rel quot_thm);
- val proved_assms = prem_rels |> map (try_prove_refl_rel ctxt)
- |> map_index (apfst (fn x => x + 1)) |> filter (is_some o snd) |> map (apsnd the)
+ val proved_assms = prem_rels |> map (try_prove_refl_rel ctxt)
+ |> map_index (apfst (fn x => x + 1)) |> filter (is_some o snd) |> map (apsnd the)
|> map (apsnd (fn assm => assm RS @{thm ge_eq_refl}))
val abs_eq = fold_rev (fn (i, assm) => fn thm => assm RSN (i, thm)) proved_assms abs_eq_with_assms
in
@@ -445,7 +445,7 @@
| no_abstr (Abs (_, _, t)) = no_abstr t
| no_abstr (Const (name, _)) = not (Code.is_abstr thy name)
| no_abstr _ = true
- fun is_valid_eq eqn = can (Code.assert_eqn thy) (mk_meta_eq eqn, true)
+ fun is_valid_eq eqn = can (Code.assert_eqn thy) (mk_meta_eq eqn, true)
andalso no_abstr (Thm.prop_of eqn)
fun is_valid_abs_eq abs_eq = can (Code.assert_abs_eqn thy NONE) (mk_meta_eq abs_eq)
@@ -474,8 +474,8 @@
else
if is_Type qty then
if Lifting_Info.is_no_code_type ctxt (Tname qty) then false
- else
- let
+ else
+ let
val (rty', rtyq) = Lifting_Term.instantiate_rtys ctxt (rty, qty)
val (rty's, rtyqs) = (Targs rty', Targs rtyq)
in
@@ -484,26 +484,26 @@
else
true
- fun encode_code_eq ctxt abs_eq opt_rep_eq (rty, qty) =
+ fun encode_code_eq ctxt abs_eq opt_rep_eq (rty, qty) =
let
fun mk_type typ = typ |> Logic.mk_type |> Thm.cterm_of ctxt |> Drule.mk_term
in
Conjunction.intr_balanced [abs_eq, (the_default TrueI opt_rep_eq), mk_type rty, mk_type qty]
end
-
+
exception DECODE
-
+
fun decode_code_eq thm =
- if Thm.nprems_of thm > 0 then raise DECODE
+ if Thm.nprems_of thm > 0 then raise DECODE
else
let
val [abs_eq, rep_eq, rty, qty] = Conjunction.elim_balanced 4 thm
val opt_rep_eq = if Thm.eq_thm_prop (rep_eq, TrueI) then NONE else SOME rep_eq
fun dest_type typ = typ |> Drule.dest_term |> Thm.term_of |> Logic.dest_type
in
- (abs_eq, opt_rep_eq, (dest_type rty, dest_type qty))
+ (abs_eq, opt_rep_eq, (dest_type rty, dest_type qty))
end
-
+
structure Data = Generic_Data
(
type T = code_eq option
@@ -520,7 +520,7 @@
Context.theory_map (Data.put (SOME code_eq)) thy
end
handle DECODE => thy
-
+
val register_code_eq_attribute = Thm.declaration_attribute
(fn thm => Context.mapping (register_encoded_code_eq thm) I)
val register_code_eq_attrib = Attrib.internal (K register_code_eq_attribute)
@@ -533,14 +533,15 @@
in
if no_no_code lthy (rty, qty) then
let
- val lthy = (snd oo Local_Theory.note)
+ val lthy = (snd oo Local_Theory.note)
((Binding.empty, [register_code_eq_attrib]), [encoded_code_eq]) lthy
val opt_code_eq = Data.get (Context.Theory (Proof_Context.theory_of lthy))
- val code_eq = if is_some opt_code_eq then the opt_code_eq
+ val code_eq =
+ if is_some opt_code_eq then the opt_code_eq
else UNKNOWN_EQ (* UNKNOWN_EQ means that we are in a locale and we do not know
which code equation is going to be used. This is going to be resolved at the
point when an interpretation of the locale is executed. *)
- val lthy = Local_Theory.declaration {syntax = false, pervasive = true}
+ val lthy = Local_Theory.declaration {syntax = false, pervasive = true}
(K (Data.put NONE)) lthy
in
(code_eq, lthy)
@@ -549,9 +550,9 @@
(NONE_EQ, lthy)
end
end
-
+
(*
- Defines an operation on an abstract type in terms of a corresponding operation
+ Defines an operation on an abstract type in terms of a corresponding operation
on a representation type.
var - a binding and a mixfix of the new constant being defined
@@ -575,8 +576,8 @@
val (_, newrhs) = Local_Defs.abs_def prop'
val var = ((#notes config = false ? Binding.concealed) binding, mx)
val def_name = Thm.make_def_binding (#notes config) (#1 var)
-
- val ((lift_const, (_ , def_thm)), lthy) =
+
+ val ((lift_const, (_ , def_thm)), lthy) =
Local_Theory.define (var, ((def_name, []), newrhs)) lthy
val transfer_rules = generate_transfer_rules lthy quot_thm rsp_thm def_thm par_thms
@@ -591,18 +592,18 @@
val abs_eq_thmN = Binding.qualify_name true lhs_name "abs_eq"
val rep_eq_thmN = Binding.qualify_name true lhs_name "rep_eq"
val transfer_ruleN = Binding.qualify_name true lhs_name "transfer"
- val notes =
- [(rsp_thmN, [], [rsp_thm]),
+ val notes =
+ [(rsp_thmN, [], [rsp_thm]),
(transfer_ruleN, @{attributes [transfer_rule]}, transfer_rules),
- (abs_eq_thmN, [], [abs_eq_thm])]
+ (abs_eq_thmN, [], [abs_eq_thm])]
@ (case opt_rep_eq_thm of SOME rep_eq_thm => [(rep_eq_thmN, [], [rep_eq_thm])] | NONE => [])
in
if names then map (fn (name, attrs, thms) => ((name, []), [(thms, attrs)])) notes
- else map_filter (fn (_, attrs, thms) => if null attrs then NONE
- else SOME ((Binding.empty, []), [(thms, attrs)])) notes
+ else map_filter (fn (_, attrs, thms) => if null attrs then NONE
+ else SOME (Binding.empty_atts, [(thms, attrs)])) notes
end
val (code_eq, lthy) = register_code_eq abs_eq_thm opt_rep_eq_thm (rty_forced, qty) lthy
- val lift_def = mk_lift_def rty_forced qty newrhs lift_const def_thm rsp_thm abs_eq_thm
+ val lift_def = mk_lift_def rty_forced qty newrhs lift_const def_thm rsp_thm abs_eq_thm
opt_rep_eq_thm code_eq transfer_rules
in
lthy
@@ -616,8 +617,8 @@
fun get_cr_pcr_eqs ctxt =
let
fun collect (data : Lifting_Info.quotient) l =
- if is_some (#pcr_info data)
- then ((Thm.symmetric o safe_mk_meta_eq o #pcr_cr_eq o the o #pcr_info) data :: l)
+ if is_some (#pcr_info data)
+ then ((Thm.symmetric o safe_mk_meta_eq o #pcr_cr_eq o the o #pcr_info) data :: l)
else l
val table = Lifting_Info.get_quotients ctxt
in
@@ -629,7 +630,7 @@
val rsp_rel = Lifting_Term.equiv_relation lthy (fastype_of rhs, qty)
val rty_forced = (domain_type o fastype_of) rsp_rel;
val forced_rhs = force_rty_type lthy rty_forced rhs;
- val cr_to_pcr_conv = HOLogic.Trueprop_conv (Conv.fun2_conv
+ val cr_to_pcr_conv = HOLogic.Trueprop_conv (Conv.fun2_conv
(Raw_Simplifier.rewrite lthy false (get_cr_pcr_eqs lthy)))
val (prsp_tm, rsp_prsp_eq) = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs)
|> Thm.cterm_of lthy
@@ -639,13 +640,13 @@
|>> snd
val to_rsp = rsp_prsp_eq RS Drule.equal_elim_rule2
val opt_proven_rsp_thm = try_prove_reflexivity lthy prsp_tm
-
- fun after_qed internal_rsp_thm lthy =
+
+ fun after_qed internal_rsp_thm lthy =
add_lift_def var qty rhs (internal_rsp_thm RS to_rsp) par_thms lthy
in
case opt_proven_rsp_thm of
SOME thm => (NONE, K (after_qed thm))
- | NONE => (SOME prsp_tm, after_qed)
+ | NONE => (SOME prsp_tm, after_qed)
end
fun gen_lift_def add_lift_def var qty rhs tac par_thms lthy =
@@ -653,8 +654,8 @@
val (goal, after_qed) = prepare_lift_def add_lift_def var qty rhs par_thms lthy
in
case goal of
- SOME goal =>
- let
+ SOME goal =>
+ let
val rsp_thm = Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => tac ctxt)
|> Thm.close_derivation
in
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Thu Jun 23 11:01:14 2016 +0200
@@ -298,8 +298,9 @@
EVERY' [Transfer.gen_frees_tac [] ctxt, DETERM o Transfer.transfer_tac true ctxt,
SELECT_GOAL (Local_Defs.unfold0_tac ctxt [id_apply]), rtac ctxt refl] i;
val rep_isom_transfer = transfer_of_rep_isom_data rep_isom_data
- val (_, transfer_lthy) = Proof_Context.note_thmss "" [((Binding.empty, []),
- [([rep_isom_transfer], [Transfer.transfer_add])])] lthy
+ val (_, transfer_lthy) =
+ Proof_Context.note_thmss ""
+ [(Binding.empty_atts, [([rep_isom_transfer], [Transfer.transfer_add])])] lthy
val f_alt_def = Goal.prove_sorry transfer_lthy [] [] f_alt_def_goal
(fn {context = ctxt, prems = _} => HEADGOAL (f_alt_def_tac ctxt))
|> Thm.close_derivation
@@ -444,9 +445,10 @@
(map safe_mk_meta_eq @{thms id_apply simp_thms Ball_def}),
rtac ctxt TrueI] i;
- val (_, transfer_lthy) = Proof_Context.note_thmss "" [((Binding.empty, []),
- [(@{thms right_total_UNIV_transfer},[Transfer.transfer_add]),
- (@{thms Domain_eq_top}, [Transfer.transfer_domain_add]) ])] lthy;
+ val (_, transfer_lthy) =
+ Proof_Context.note_thmss "" [(Binding.empty_atts,
+ [(@{thms right_total_UNIV_transfer},[Transfer.transfer_add]),
+ (@{thms Domain_eq_top}, [Transfer.transfer_domain_add])])] lthy;
val quot_thm_isom = Goal.prove_sorry transfer_lthy [] [] typedef_goal
(fn {context = ctxt, prems = _} => typ_isom_tac ctxt 1)
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Thu Jun 23 11:01:14 2016 +0200
@@ -45,10 +45,13 @@
val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
val crel_name = Binding.prefix_name "cr_" qty_name
val (fixed_def_term, lthy) = yield_singleton (Variable.importT_terms) def_term lthy
- val ((_, (_ , def_thm)), lthy) = if #notes config then
- Local_Theory.define ((crel_name, NoSyn), ((Thm.def_binding crel_name, []), fixed_def_term)) lthy
+ val ((_, (_ , def_thm)), lthy) =
+ if #notes config then
+ Local_Theory.define
+ ((crel_name, NoSyn), ((Thm.def_binding crel_name, []), fixed_def_term)) lthy
else
- Local_Theory.define ((Binding.concealed crel_name, NoSyn), ((Binding.empty, []), fixed_def_term)) lthy
+ Local_Theory.define
+ ((Binding.concealed crel_name, NoSyn), (Binding.empty_atts, fixed_def_term)) lthy
in
(def_thm, lthy)
end
@@ -90,12 +93,13 @@
val definition_term = Logic.mk_equals (lhs, rhs)
fun note_def lthy =
Specification.definition (SOME (pcrel_name, SOME relator_type, NoSyn)) [] []
- ((Binding.empty, []), definition_term) lthy |>> (snd #> snd);
+ (Binding.empty_atts, definition_term) lthy |>> (snd #> snd);
fun raw_def lthy =
let
val ((_, rhs), prove) = Local_Defs.derived_def lthy {conditional = true} definition_term;
- val ((_, (_, raw_th)), lthy) = lthy
- |> Local_Theory.define ((Binding.concealed pcrel_name, NoSyn), ((Binding.empty, []), rhs));
+ val ((_, (_, raw_th)), lthy) =
+ Local_Theory.define
+ ((Binding.concealed pcrel_name, NoSyn), (Binding.empty_atts, rhs)) lthy;
val th = prove lthy raw_th;
in
(th, lthy)
@@ -498,9 +502,9 @@
fun notes names thms =
let
val notes =
- if names then map (fn (name, thms, attrs) => ((name, []), [(thms, attrs)])) thms
- else map_filter (fn (_, thms, attrs) => if null attrs then NONE
- else SOME ((Binding.empty, []), [(thms, attrs)])) thms
+ if names then map (fn (name, thms, attrs) => ((name, []), [(thms, attrs)])) thms
+ else map_filter (fn (_, thms, attrs) => if null attrs then NONE
+ else SOME (Binding.empty_atts, [(thms, attrs)])) thms
in
Local_Theory.notes notes #> snd
end
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Thu Jun 23 11:01:14 2016 +0200
@@ -177,7 +177,7 @@
{quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
coind = false, no_elim = true, no_ind = false, skip_mono = true}
(map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
- (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
+ (map (fn x => (Binding.empty_atts, x)) intr_ts) []
||> Sign.restore_naming thy1;
(********************************* typedef ********************************)
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Thu Jun 23 11:01:14 2016 +0200
@@ -155,7 +155,7 @@
coind = false, no_elim = false, no_ind = true, skip_mono = true}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
- (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
+ (map (fn x => (Binding.empty_atts, x)) rec_intr_ts) []
||> Sign.restore_naming thy0;
(* prove uniqueness and termination of primrec combinators *)
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Thu Jun 23 11:01:14 2016 +0200
@@ -374,7 +374,7 @@
else
fold_map (fn (name, T) => Local_Theory.define
((Binding.concealed (Binding.name name), NoSyn),
- (apfst Binding.concealed Attrib.empty_binding, mk_undefined T))
+ (apfst Binding.concealed Binding.empty_atts, mk_undefined T))
#> apfst fst) (names ~~ Ts)
#> (fn (consts, lthy) =>
let
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Thu Jun 23 11:01:14 2016 +0200
@@ -141,7 +141,7 @@
val proj_eqs = map2 (fn v => fn proj => (v, lambda arg proj)) vs projs;
val proj_defs = map2 (fn Free (name, _) => fn (_, rhs) =>
((Binding.concealed (Binding.name name), NoSyn),
- (apfst Binding.concealed Attrib.empty_binding, rhs))) vs proj_eqs;
+ (apfst Binding.concealed Binding.empty_atts, rhs))) vs proj_eqs;
val aux_eq' = Pattern.rewrite_term thy proj_eqs [] aux_eq;
fun prove_eqs aux_simp proj_defs lthy =
let
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Thu Jun 23 11:01:14 2016 +0200
@@ -133,7 +133,7 @@
(* relator_eq *)
fun relator_eq bnf =
- [((Binding.empty, []), [([rel_eq_of_bnf bnf], @{attributes [relator_eq]})])]
+ [(Binding.empty_atts, [([rel_eq_of_bnf bnf], @{attributes [relator_eq]})])]
(* transfer rules *)
@@ -143,7 +143,7 @@
:: rel_transfer_of_bnf bnf :: set_transfer_of_bnf bnf
val transfer_attr = @{attributes [transfer_rule]}
in
- map (fn thm => ((Binding.empty,[]),[([thm],transfer_attr)])) transfer_rules
+ map (fn thm => (Binding.empty_atts, [([thm],transfer_attr)])) transfer_rules
end
(* Domainp theorem for predicator *)
@@ -251,7 +251,7 @@
@ (#co_rec_transfers o #fp_co_induct_sugar) fp_sugar
val transfer_attr = @{attributes [transfer_rule]}
in
- map (fn thm => ((Binding.empty, []), [([thm], transfer_attr)])) transfer_rules
+ map (fn thm => (Binding.empty_atts, [([thm], transfer_attr)])) transfer_rules
end
fun register_pred_injects fp_sugar lthy =
--- a/src/HOL/Tools/record.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Tools/record.ML Thu Jun 23 11:01:14 2016 +0200
@@ -1781,7 +1781,7 @@
|> fold (Code.add_eqn (Code.Equation, true)) simps
|> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition NONE [] [] (Attrib.empty_binding, eq))
+ |-> (fn eq => Specification.definition NONE [] [] (Binding.empty_atts, eq))
|-> (fn (_, (_, eq_def)) =>
Class.prove_instantiation_exit_result Morphism.thm tac eq_def)
|-> (fn eq_def => fn thy =>
--- a/src/HOL/Typerep.thy Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Typerep.thy Thu Jun 23 11:01:14 2016 +0200
@@ -58,7 +58,7 @@
thy
|> Class.instantiation ([tyco], vs, @{sort typerep})
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition NONE [] [] (Attrib.empty_binding, eq))
+ |-> (fn eq => Specification.definition NONE [] [] (Binding.empty_atts, eq))
|> snd
|> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
end;
--- a/src/Pure/General/binding.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/Pure/General/binding.ML Thu Jun 23 11:01:14 2016 +0200
@@ -25,6 +25,8 @@
val eq_name: binding * binding -> bool
val empty: binding
val is_empty: binding -> bool
+ val empty_atts: binding * 'a list
+ val is_empty_atts: binding * 'a list -> bool
val conglomerate: binding list -> binding
val qualify: bool -> string -> binding -> binding
val qualify_name: bool -> binding -> string -> binding
@@ -102,6 +104,9 @@
val empty = name "";
fun is_empty b = name_of b = "";
+val empty_atts = (empty, []);
+fun is_empty_atts (b, atts) = is_empty b andalso null atts;
+
fun conglomerate [b] = b
| conglomerate bs = name (space_implode "_" (map name_of bs));
--- a/src/Pure/Isar/attrib.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/Pure/Isar/attrib.ML Thu Jun 23 11:01:14 2016 +0200
@@ -6,8 +6,6 @@
signature ATTRIB =
sig
- val empty_binding: Attrib.binding
- val is_empty_binding: Attrib.binding -> bool
val print_attributes: bool -> Proof.context -> unit
val define_global: binding -> (Token.src -> attribute) -> string -> theory -> string * theory
val define: binding -> (Token.src -> attribute) -> string -> local_theory -> string * local_theory
@@ -80,13 +78,8 @@
structure Attrib: sig type binding = Attrib.binding include ATTRIB end =
struct
-(* source and bindings *)
-
type binding = Attrib.binding;
-val empty_binding: binding = (Binding.empty, []);
-fun is_empty_binding ((b, srcs): binding) = Binding.is_empty b andalso null srcs;
-
(** named attributes **)
@@ -199,8 +192,8 @@
fun eval_thms ctxt srcs = ctxt
|> Proof_Context.note_thmss ""
- (map_facts_refs (map (attribute_cmd ctxt)) (Proof_Context.get_fact ctxt)
- [((Binding.empty, []), srcs)])
+ (map_facts_refs
+ (map (attribute_cmd ctxt)) (Proof_Context.get_fact ctxt) [(Binding.empty_atts, srcs)])
|> fst |> maps snd;
@@ -362,10 +355,10 @@
if eq_list (eq_fst Thm.eq_thm_strict) (decls', fact') then
[((b, []), map2 (fn (th, atts1) => fn (_, atts2) => (th, atts1 @ atts2)) decls' fact')]
else if null decls' then [((b, []), fact')]
- else [(empty_binding, decls'), ((b, []), fact')];
+ else [(Binding.empty_atts, decls'), ((b, []), fact')];
in (facts', context') end)
|> fst |> flat |> map (apsnd (map (apfst single)))
- |> filter_out (fn (b, fact) => is_empty_binding b andalso forall (null o #2) fact);
+ |> filter_out (fn (b, fact) => Binding.is_empty_atts b andalso forall (null o #2) fact);
end;
--- a/src/Pure/Isar/bundle.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/Pure/Isar/bundle.ML Thu Jun 23 11:01:14 2016 +0200
@@ -112,7 +112,7 @@
val bundle0 = raw_bundle
|> map (fn (fact, atts) => (prep_fact ctxt' fact, map (prep_att ctxt') atts));
val bundle =
- Attrib.partial_evaluation ctxt' [(Attrib.empty_binding, bundle0)] |> map snd |> flat
+ Attrib.partial_evaluation ctxt' [(Binding.empty_atts, bundle0)] |> map snd |> flat
|> transform_bundle (Proof_Context.export_morphism ctxt' lthy);
in
lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
@@ -200,7 +200,7 @@
let val decls = maps (get ctxt) args in
ctxt
|> Context_Position.set_visible false
- |> notes [((Binding.empty, []), decls)] |> #2
+ |> notes [(Binding.empty_atts, decls)] |> #2
|> Context_Position.restore_visible ctxt
end;
--- a/src/Pure/Isar/class_declaration.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/Pure/Isar/class_declaration.ML Thu Jun 23 11:01:14 2016 +0200
@@ -298,14 +298,14 @@
| [thm] => SOME thm);
in
thy
- |> add_consts class base_sort sups supparam_names global_syntax
- |-> (fn (param_map, params) => Axclass.define_class (bname, supsort)
- (map (fst o snd) params)
- [(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)]
- #> snd
- #> `get_axiom
- #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
- #> pair (param_map, params, assm_axiom)))
+ |> add_consts class base_sort sups supparam_names global_syntax |-> (fn (param_map, params) =>
+ Axclass.define_class (bname, supsort)
+ (map (fst o snd) params)
+ [(Binding.empty_atts, Option.map (globalize param_map) raw_pred |> the_list)]
+ #> snd
+ #> `get_axiom
+ #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
+ #> pair (param_map, params, assm_axiom)))
end;
fun gen_class prep_class_spec b raw_supclasses raw_elems thy =
--- a/src/Pure/Isar/element.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/Pure/Isar/element.ML Thu Jun 23 11:01:14 2016 +0200
@@ -239,8 +239,8 @@
then insert (op =) (Variable.revert_fixed ctxt' x, T) else I | _ => I) prop []);
in
pretty_ctxt ctxt' (Fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) fixes)) @
- pretty_ctxt ctxt' (Assumes (map (fn t => (Attrib.empty_binding, [(t, [])])) assumes)) @
- (if null cases then pretty_stmt ctxt' (Shows [(Attrib.empty_binding, [(concl, [])])])
+ pretty_ctxt ctxt' (Assumes (map (fn t => (Binding.empty_atts, [(t, [])])) assumes)) @
+ (if null cases then pretty_stmt ctxt' (Shows [(Binding.empty_atts, [(concl, [])])])
else
let val (clauses, ctxt'') = fold_map obtain cases ctxt'
in pretty_stmt ctxt'' (Obtains clauses) end)
@@ -293,7 +293,7 @@
in
Proof.map_context (K goal_ctxt) #>
Proof.internal_goal (K (K ())) (Proof_Context.get_mode goal_ctxt) true cmd
- NONE after_qed' [] [] (map (pair Thm.empty_binding) propp) #> snd
+ NONE after_qed' [] [] (map (pair Binding.empty_atts) propp) #> snd
end;
in
--- a/src/Pure/Isar/expression.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/Pure/Isar/expression.ML Thu Jun 23 11:01:14 2016 +0200
@@ -591,10 +591,10 @@
val text' =
text |>
(if is_some asm then
- eval_text ctxt false (Assumes [(Attrib.empty_binding, [(the asm', [])])])
+ eval_text ctxt false (Assumes [(Binding.empty_atts, [(the asm', [])])])
else I) |>
(if not (null defs) then
- eval_text ctxt false (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs'))
+ eval_text ctxt false (Defines (map (fn def => (Binding.empty_atts, (def, []))) defs'))
else I)
(* FIXME clone from locale.ML *)
in text' end;
--- a/src/Pure/Isar/generic_target.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/Pure/Isar/generic_target.ML Thu Jun 23 11:01:14 2016 +0200
@@ -243,7 +243,7 @@
(*local definition*)
val ([(lhs, (_, local_def))], lthy3) = lthy2
|> Context_Position.set_visible false
- |> Local_Defs.define [((b, NoSyn), (Thm.empty_binding, lhs'))]
+ |> Local_Defs.define [((b, NoSyn), (Binding.empty_atts, lhs'))]
||> Context_Position.restore_visible lthy2;
(*result*)
--- a/src/Pure/Isar/interpretation.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/Pure/Isar/interpretation.ML Thu Jun 23 11:01:14 2016 +0200
@@ -120,7 +120,7 @@
fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt =
let
- val facts = (Attrib.empty_binding, [(map (Morphism.thm (export' $> export)) def_eqns, [])])
+ val facts = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])])
:: map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
val (eqns', ctxt') = ctxt
|> note Thm.theoremK facts
--- a/src/Pure/Isar/locale.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/Pure/Isar/locale.ML Thu Jun 23 11:01:14 2016 +0200
@@ -437,9 +437,9 @@
(not (null params) ?
activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
(* FIXME type parameters *)
- (case asm of SOME A => activ_elem (Assumes [(Attrib.empty_binding, [(A, [])])]) | _ => I) |>
+ (case asm of SOME A => activ_elem (Assumes [(Binding.empty_atts, [(A, [])])]) | _ => I) |>
(not (null defs) ?
- activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs)));
+ activ_elem (Defines (map (fn def => (Binding.empty_atts, (def, []))) defs)));
val activate = activate_notes activ_elem transfer (Context.Theory thy) NONE;
in
roundup thy activate Morphism.identity (name, Morphism.identity) (marked, input')
@@ -615,7 +615,7 @@
fun add_declaration loc syntax decl =
syntax ?
Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
- #> add_thmss loc "" [(Attrib.empty_binding, Attrib.internal_declaration decl)];
+ #> add_thmss loc "" [(Binding.empty_atts, Attrib.internal_declaration decl)];
(*** Reasoning about locales ***)
--- a/src/Pure/Isar/named_target.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/Pure/Isar/named_target.ML Thu Jun 23 11:01:14 2016 +0200
@@ -109,7 +109,7 @@
map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
(#1 (Proof_Context.inferred_fixes ctxt));
val assumes =
- map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
+ map (fn A => (Binding.empty_atts, [(Thm.term_of A, [])]))
(Assumption.all_assms_of ctxt);
val elems =
(if null fixes then [] else [Element.Fixes fixes]) @
--- a/src/Pure/Isar/obtain.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/Pure/Isar/obtain.ML Thu Jun 23 11:01:14 2016 +0200
@@ -228,7 +228,7 @@
|> Proof.have true NONE after_qed
[(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
[((that_binding, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
- [(Thm.empty_binding, [(thesis, [])])] int
+ [(Binding.empty_atts, [(thesis, [])])] int
|-> Proof.refine_insert
|> Proof.map_context (fold Variable.bind_term binds')
end;
@@ -376,7 +376,7 @@
|> Proof.fix (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
|> `Proof.context_of |-> (fn fix_ctxt => Proof.assm
(obtain_export fix_ctxt rule (map (Thm.cterm_of ctxt) ts))
- [] [] [(Thm.empty_binding, asms)])
+ [] [] [(Binding.empty_atts, asms)])
|> Proof.map_context (fold Variable.unbind_term Auto_Bind.no_facts)
end;
@@ -403,7 +403,7 @@
|> Proof.chain_facts chain_facts
|> Proof.internal_goal print_result Proof_Context.mode_schematic true "guess"
(SOME before_qed) after_qed
- [] [] [(Thm.empty_binding, [(Logic.mk_term goal, []), (goal, [])])]
+ [] [] [(Binding.empty_atts, [(Logic.mk_term goal, []), (goal, [])])]
|> snd
|> Proof.refine_singleton
(Method.primitive_text (fn _ => fn _ => Goal.init (Thm.cterm_of ctxt thesis)))
--- a/src/Pure/Isar/parse_spec.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/Pure/Isar/parse_spec.ML Thu Jun 23 11:01:14 2016 +0200
@@ -46,7 +46,7 @@
fun opt_thm_name s =
Scan.optional
((Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty) --| Parse.$$$ s)
- Attrib.empty_binding;
+ Binding.empty_atts;
val simple_spec = opt_thm_name ":" -- Parse.prop;
val simple_specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop;
--- a/src/Pure/Isar/proof.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/Pure/Isar/proof.ML Thu Jun 23 11:01:14 2016 +0200
@@ -728,7 +728,7 @@
(* note etc. *)
-fun no_binding args = map (pair (Binding.empty, [])) args;
+fun empty_bindings args = map (pair Binding.empty_atts) args;
local
@@ -746,13 +746,13 @@
val note_thmss = gen_thmss (K []) I #2 (K I) (K I);
val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute_cmd Proof_Context.get_fact;
-val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
+val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o empty_bindings;
val from_thmss_cmd =
- gen_thmss (K []) chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding;
+ gen_thmss (K []) chain #2 Attrib.attribute_cmd Proof_Context.get_fact o empty_bindings;
-val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
+val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o empty_bindings;
val with_thmss_cmd =
- gen_thmss the_facts chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding;
+ gen_thmss the_facts chain #2 Attrib.attribute_cmd Proof_Context.get_fact o empty_bindings;
val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
@@ -786,7 +786,7 @@
|> assert_backward
|> map_context_result
(fn ctxt => ctxt |> Proof_Context.note_thmss ""
- (Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) (no_binding args)))
+ (Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) (empty_bindings args)))
|> (fn (named_facts, state') =>
state' |> map_goal (fn (goal_ctxt, statement, using, goal, before_qed, after_qed) =>
let
@@ -855,7 +855,7 @@
(*defs*)
fun match_defs (((b, _, mx), (_, Free (x, T))) :: more_decls) ((((y, U), t), _) :: more_defs) =
- if x = y then ((b, mx), (Thm.empty_binding, t)) :: match_defs more_decls more_defs
+ if x = y then ((b, mx), (Binding.empty_atts, t)) :: match_defs more_decls more_defs
else
error ("Mismatch of declaration " ^ show_term (Free (x, T)) ^ " wrt. definition " ^
show_term (Free (y, U)))
--- a/src/Pure/Isar/specification.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/Pure/Isar/specification.ML Thu Jun 23 11:01:14 2016 +0200
@@ -378,7 +378,7 @@
|> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.thatN, []), [(that, [])])]
||> Proof_Context.restore_stmt asms_ctxt;
- val stmt' = [((Binding.empty, []), [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])])];
+ val stmt' = [(Binding.empty_atts, [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])])];
in ((Obtain.obtains_attribs raw_obtains, prems, stmt', SOME that'), that_ctxt) end)
end;
@@ -399,12 +399,12 @@
val results' =
burrow (map (Goal.norm_result lthy) o Proof_Context.export goal_ctxt' lthy) results;
val (res, lthy') =
- if forall (Attrib.is_empty_binding o fst) stmt then (map (pair "") results', lthy)
+ if forall (Binding.is_empty_atts o fst) stmt then (map (pair "") results', lthy)
else
Local_Theory.notes_kind kind
(map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;
val lthy'' =
- if Attrib.is_empty_binding (name, atts) then
+ if Binding.is_empty_atts (name, atts) then
(Proof_Display.print_results int pos lthy' ((kind, ""), res); lthy')
else
let
--- a/src/Pure/Isar/subgoal.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/Pure/Isar/subgoal.ML Thu Jun 23 11:01:14 2016 +0200
@@ -207,7 +207,7 @@
val (prems_binding, do_prems) =
(case raw_prems_binding of
SOME (b, raw_atts) => ((b, map (prep_atts ctxt) raw_atts), true)
- | NONE => ((Binding.empty, []), false));
+ | NONE => (Binding.empty_atts, false));
val (subgoal_focus, _) =
(if do_prems then focus else focus_params_fixed) ctxt
@@ -239,7 +239,7 @@
#context subgoal_focus
|> Proof_Context.note_thmss "" [(prems_binding, [(#prems subgoal_focus, [])])] |> #2)
|> Proof.internal_goal (K (K ())) (Proof_Context.get_mode ctxt) true "subgoal"
- NONE after_qed [] [] [(Thm.empty_binding, [(Thm.term_of (#concl subgoal_focus), [])])] |> #2
+ NONE after_qed [] [] [(Binding.empty_atts, [(Thm.term_of (#concl subgoal_focus), [])])] |> #2
|> Proof.using_facts facts
|> pair subgoal_focus
end;
--- a/src/Pure/Pure.thy Wed Jun 22 16:04:03 2016 +0200
+++ b/src/Pure/Pure.thy Thu Jun 23 11:01:14 2016 +0200
@@ -408,14 +408,14 @@
Parse_Spec.long_statement_keyword;
val long_statement =
- Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Attrib.empty_binding --
+ Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Binding.empty_atts --
Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement
>> (fn ((binding, includes), (elems, concl)) => (true, binding, includes, elems, concl));
val short_statement =
Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes
>> (fn ((shows, assumes), fixes) =>
- (false, Attrib.empty_binding, [], [Element.Fixes fixes, Element.Assumes assumes],
+ (false, Binding.empty_atts, [], [Element.Fixes fixes, Element.Assumes assumes],
Element.Shows shows));
fun theorem spec schematic descr =
@@ -444,7 +444,7 @@
Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems"
(Parse.and_list1 Parse.thms1 -- Parse.for_fixes
>> (fn (facts, fixes) =>
- #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
+ #2 oo Specification.theorems_cmd "" [(Binding.empty_atts, flat facts)] fixes));
val _ =
Outer_Syntax.local_theory @{command_keyword named_theorems}
@@ -915,7 +915,7 @@
val opt_fact_binding =
Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty)
- Attrib.empty_binding;
+ Binding.empty_atts;
val for_params =
Scan.optional
--- a/src/Pure/more_thm.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/Pure/more_thm.ML Thu Jun 23 11:01:14 2016 +0200
@@ -83,7 +83,6 @@
val add_def_global: bool -> bool -> binding * term -> theory -> (string * thm) * theory
type attribute = Context.generic * thm -> Context.generic option * thm option
type binding = binding * attribute list
- val empty_binding: binding
val tag_rule: string * string -> thm -> thm
val untag_rule: string -> thm -> thm
val is_free_dummy: thm -> bool
@@ -597,7 +596,6 @@
type attribute = Context.generic * thm -> Context.generic option * thm option;
type binding = binding * attribute list;
-val empty_binding: binding = (Binding.empty, []);
fun rule_attribute ths f (x, th) =
(NONE,