tuned signature;
authorwenzelm
Thu Jun 23 11:01:14 2016 +0200 (2016-06-23)
changeset 633524eaf35781b23
parent 63347 e344dc82f6c2
child 63353 176d1f408696
tuned signature;
NEWS
src/HOL/HOLCF/Tools/fixrec.ML
src/HOL/Library/simps_case_conv.ML
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/SPARK/Tools/spark_vcs.ML
src/HOL/Tools/BNF/bnf_gfp_grec.ML
src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
src/HOL/Tools/Function/fun.ML
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Lifting/lifting_bnf.ML
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_def_code_dt.ML
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/Old_Datatype/old_datatype.ML
src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/Transfer/transfer_bnf.ML
src/HOL/Tools/record.ML
src/HOL/Typerep.thy
src/Pure/General/binding.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/bundle.ML
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/interpretation.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/named_target.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/parse_spec.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/subgoal.ML
src/Pure/Pure.thy
src/Pure/more_thm.ML
     1.1 --- a/NEWS	Wed Jun 22 16:04:03 2016 +0200
     1.2 +++ b/NEWS	Thu Jun 23 11:01:14 2016 +0200
     1.3 @@ -478,6 +478,9 @@
     1.4  relatively to the master directory of a theory (see also
     1.5  File.full_path). Potential INCOMPATIBILITY.
     1.6  
     1.7 +* Binding.empty_atts supersedes Thm.empty_binding and
     1.8 +Attrib.empty_binding. Minor INCOMPATIBILITY.
     1.9 +
    1.10  
    1.11  *** System ***
    1.12  
     2.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Wed Jun 22 16:04:03 2016 +0200
     2.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Thu Jun 23 11:01:14 2016 +0200
     2.3 @@ -356,7 +356,7 @@
     2.4          | NONE => fixrec_err ("unknown pattern constructor: " ^ c)
     2.5  
     2.6      val matches = map (compile_eqs match_name) (map (map (snd o fst)) blocks)
     2.7 -    val spec' = map (pair Attrib.empty_binding) matches
     2.8 +    val spec' = map (pair Binding.empty_atts) matches
     2.9      val (lthy, _, _, unfold_thms) =
    2.10        add_fixdefs fixes spec' lthy
    2.11  
    2.12 @@ -388,7 +388,7 @@
    2.13  (*************************************************************************)
    2.14  
    2.15  val opt_thm_name' : (bool * Attrib.binding) parser =
    2.16 -  @{keyword "("} -- @{keyword "unchecked"} -- @{keyword ")"} >> K (true, Attrib.empty_binding)
    2.17 +  @{keyword "("} -- @{keyword "unchecked"} -- @{keyword ")"} >> K (true, Binding.empty_atts)
    2.18      || Parse_Spec.opt_thm_name ":" >> pair false
    2.19  
    2.20  val spec' : (bool * (Attrib.binding * string)) parser =
     3.1 --- a/src/HOL/Library/simps_case_conv.ML	Wed Jun 22 16:04:03 2016 +0200
     3.2 +++ b/src/HOL/Library/simps_case_conv.ML	Thu Jun 23 11:01:14 2016 +0200
     3.3 @@ -137,7 +137,7 @@
     3.4          val frees = fold Term.add_frees pat []
     3.5          val abs_rhs = fold absfree frees rhs
     3.6          val ([(f, (_, def))], lthy') = lthy
     3.7 -          |> Local_Defs.define [((Binding.name name, NoSyn), (Thm.empty_binding, abs_rhs))]
     3.8 +          |> Local_Defs.define [((Binding.name name, NoSyn), (Binding.empty_atts, abs_rhs))]
     3.9        in ((list_comb (f, map Free (rev frees)), def), lthy') end
    3.10  
    3.11      val ((def_ts, def_thms), ctxt2) =
     4.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Jun 22 16:04:03 2016 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Jun 23 11:01:14 2016 +0200
     4.3 @@ -192,7 +192,7 @@
     4.4          thy' |>
     4.5          BNF_LFP_Compat.primrec_global
     4.6            [(Binding.name swap_name, SOME swapT, NoSyn)]
     4.7 -          [((Attrib.empty_binding, def1), [], [])] ||>
     4.8 +          [((Binding.empty_atts, def1), [], [])] ||>
     4.9          Sign.parent_path ||>>
    4.10          Global_Theory.add_defs_unchecked true
    4.11            [((Binding.name name, def2), [])] |>> (snd o fst)
    4.12 @@ -226,7 +226,7 @@
    4.13          thy' |>
    4.14          BNF_LFP_Compat.primrec_global
    4.15            [(Binding.name prm_name, SOME prmT, NoSyn)]
    4.16 -          (map (fn def => ((Attrib.empty_binding, def), [], [])) [def1, def2]) ||>
    4.17 +          (map (fn def => ((Binding.empty_atts, def), [], [])) [def1, def2]) ||>
    4.18          Sign.parent_path
    4.19        end) ak_names_types thy3;
    4.20      
     5.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Wed Jun 22 16:04:03 2016 +0200
     5.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Jun 23 11:01:14 2016 +0200
     5.3 @@ -251,7 +251,7 @@
     5.4                else Const (@{const_name Nominal.perm}, permT --> T --> T) $ pi $ x
     5.5              end;
     5.6          in
     5.7 -          ((Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
     5.8 +          ((Binding.empty_atts, HOLogic.mk_Trueprop (HOLogic.mk_eq
     5.9              (Free (nth perm_names_types' i) $
    5.10                 Free ("pi", mk_permT (TFree ("'x", @{sort type}))) $
    5.11                 list_comb (c, args),
    5.12 @@ -544,7 +544,7 @@
    5.13             coind = false, no_elim = true, no_ind = false, skip_mono = true}
    5.14            (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
    5.15               (rep_set_names' ~~ recTs'))
    5.16 -          [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
    5.17 +          [] (map (fn x => (Binding.empty_atts, x)) intr_ts) []
    5.18        ||> Sign.restore_naming thy3;
    5.19  
    5.20      (**** Prove that representing set is closed under permutation ****)
    5.21 @@ -1533,7 +1533,7 @@
    5.22             coind = false, no_elim = false, no_ind = false, skip_mono = true}
    5.23            (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    5.24            (map dest_Free rec_fns)
    5.25 -          (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
    5.26 +          (map (fn x => (Binding.empty_atts, x)) rec_intr_ts) []
    5.27        ||> Global_Theory.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct")
    5.28        ||> Sign.restore_naming thy10;
    5.29  
     6.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Jun 22 16:04:03 2016 +0200
     6.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Jun 23 11:01:14 2016 +0200
     6.3 @@ -795,7 +795,7 @@
     6.4         ((Binding.name ("H" ^ s'), []), [(prop_of e, [])])) ps),
     6.5       Element.Shows (map (fn (s', e) =>
     6.6         (if name_concl then (Binding.name ("C" ^ s'), [])
     6.7 -        else Attrib.empty_binding,
     6.8 +        else Binding.empty_atts,
     6.9          [(prop_of e, mk_pat s')])) cs))
    6.10    end;
    6.11  
     7.1 --- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Wed Jun 22 16:04:03 2016 +0200
     7.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Thu Jun 23 11:01:14 2016 +0200
     7.3 @@ -265,7 +265,7 @@
     7.4      val (([free], [def_free], [simps_free]), (lthy, lthy_old)) = lthy
     7.5        |> Local_Theory.open_target |> snd
     7.6        |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*)
     7.7 -      |> primrec [(b, NONE, NoSyn)] (map (fn eq => ((Attrib.empty_binding, eq), [], [])) eqs)
     7.8 +      |> primrec [(b, NONE, NoSyn)] (map (fn eq => ((Binding.empty_atts, eq), [], [])) eqs)
     7.9        ||> `Local_Theory.close_target;
    7.10  
    7.11      val phi = Proof_Context.export_morphism lthy_old lthy;
     8.1 --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Wed Jun 22 16:04:03 2016 +0200
     8.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Thu Jun 23 11:01:14 2016 +0200
     8.3 @@ -285,7 +285,7 @@
     8.4    handle Fail _ => [];
     8.5  
     8.6  fun set_transfer_rule_attrs thms =
     8.7 -  snd o Local_Theory.notes [((Binding.empty, []), [(thms, transfer_rule_attrs)])];
     8.8 +  snd o Local_Theory.notes [(Binding.empty_atts, [(thms, transfer_rule_attrs)])];
     8.9  
    8.10  fun ensure_codatatype_extra fpT_name ctxt =
    8.11    (case codatatype_extra_of ctxt fpT_name of
    8.12 @@ -1995,7 +1995,7 @@
    8.13  
    8.14      val (plugins, friend, transfer) = get_options lthy opts;
    8.15      val ([((b, fun_T), mx)], [(_, eq)]) =
    8.16 -      fst (Specification.read_multi_specs raw_fixes [((Attrib.empty_binding, raw_eq), [], [])] lthy);
    8.17 +      fst (Specification.read_multi_specs raw_fixes [((Binding.empty_atts, raw_eq), [], [])] lthy);
    8.18  
    8.19      val _ = Sign.of_sort (Proof_Context.theory_of lthy) (fun_T, @{sort type}) orelse
    8.20        error ("Type of " ^ Binding.print b ^ " contains top sort");
     9.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Jun 22 16:04:03 2016 +0200
     9.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Jun 23 11:01:14 2016 +0200
     9.3 @@ -1609,7 +1609,7 @@
     9.4     || Parse.reserved "transfer" >> K Transfer_Option);
     9.5  
     9.6  val where_alt_props_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|"
     9.7 -  ((Parse.prop >> pair Attrib.empty_binding) -- Scan.option (Parse.reserved "of" |-- Parse.const)));
     9.8 +  ((Parse.prop >> pair Binding.empty_atts) -- Scan.option (Parse.reserved "of" |-- Parse.const)));
     9.9  
    9.10  val _ = Outer_Syntax.local_theory_to_proof @{command_keyword primcorecursive}
    9.11    "define primitive corecursive functions"
    10.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Wed Jun 22 16:04:03 2016 +0200
    10.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Thu Jun 23 11:01:14 2016 +0200
    10.3 @@ -93,7 +93,7 @@
    10.4            mk_Trueprop_eq (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq})
    10.5            |> Syntax.check_term lthy;
    10.6          val ((_, (_, raw_def)), lthy') =
    10.7 -          Specification.definition NONE [] [] (Attrib.empty_binding, spec) lthy;
    10.8 +          Specification.definition NONE [] [] (Binding.empty_atts, spec) lthy;
    10.9          val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy');
   10.10          val def = singleton (Proof_Context.export lthy' thy_ctxt) raw_def;
   10.11        in
    11.1 --- a/src/HOL/Tools/Function/fun.ML	Wed Jun 22 16:04:03 2016 +0200
    11.2 +++ b/src/HOL/Tools/Function/fun.ML	Thu Jun 23 11:01:14 2016 +0200
    11.3 @@ -134,7 +134,7 @@
    11.4          |> map (map snd)
    11.5  
    11.6  
    11.7 -      val bnds' = bnds @ replicate (length spliteqs - length bnds) Attrib.empty_binding
    11.8 +      val bnds' = bnds @ replicate (length spliteqs - length bnds) Binding.empty_atts
    11.9  
   11.10        (* using theorem names for case name currently disabled *)
   11.11        val case_names = map_index (fn (i, (_, es)) => mk_case_names i "" (length es)) 
    12.1 --- a/src/HOL/Tools/Function/function_core.ML	Wed Jun 22 16:04:03 2016 +0200
    12.2 +++ b/src/HOL/Tools/Function/function_core.ML	Thu Jun 23 11:01:14 2016 +0200
    12.3 @@ -450,7 +450,7 @@
    12.4              skip_mono = true}
    12.5            [binding] (* relation *)
    12.6            [] (* no parameters *)
    12.7 -          (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
    12.8 +          (map (fn t => (Binding.empty_atts, t)) intrs) (* intro rules *)
    12.9            [] (* no special monos *)
   12.10        ||> Proof_Context.restore_naming lthy
   12.11  
    13.1 --- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Wed Jun 22 16:04:03 2016 +0200
    13.2 +++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Thu Jun 23 11:01:14 2016 +0200
    13.3 @@ -82,17 +82,17 @@
    13.4  (* relator_eq_onp  *)
    13.5  
    13.6  fun relator_eq_onp bnf =
    13.7 -  [((Binding.empty, []), [([rel_eq_onp_of_bnf bnf], @{attributes [relator_eq_onp]})])]
    13.8 +  [(Binding.empty_atts, [([rel_eq_onp_of_bnf bnf], @{attributes [relator_eq_onp]})])]
    13.9  
   13.10  (* relator_mono  *)
   13.11  
   13.12  fun relator_mono bnf =
   13.13 -  [((Binding.empty, []), [([rel_mono_of_bnf bnf], @{attributes [relator_mono]})])]    
   13.14 +  [(Binding.empty_atts, [([rel_mono_of_bnf bnf], @{attributes [relator_mono]})])]    
   13.15    
   13.16  (* relator_distr  *)
   13.17  
   13.18  fun relator_distr bnf =
   13.19 -  [((Binding.empty, []), [([rel_OO_of_bnf bnf RS sym], @{attributes [relator_distr]})])]
   13.20 +  [(Binding.empty_atts, [([rel_OO_of_bnf bnf RS sym], @{attributes [relator_distr]})])]
   13.21  
   13.22  (* interpretation *)
   13.23  
    14.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed Jun 22 16:04:03 2016 +0200
    14.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Jun 23 11:01:14 2016 +0200
    14.3 @@ -29,24 +29,24 @@
    14.4    val generate_parametric_transfer_rule:
    14.5      Proof.context -> thm -> thm -> thm
    14.6  
    14.7 -  val add_lift_def: 
    14.8 -    config -> binding * mixfix -> typ -> term -> thm -> thm list -> local_theory -> 
    14.9 +  val add_lift_def:
   14.10 +    config -> binding * mixfix -> typ -> term -> thm -> thm list -> local_theory ->
   14.11        lift_def * local_theory
   14.12 -  
   14.13 +
   14.14    val prepare_lift_def:
   14.15 -    (binding * mixfix -> typ -> term -> thm -> thm list -> Proof.context -> 
   14.16 -      lift_def * local_theory) -> 
   14.17 -    binding * mixfix -> typ -> term -> thm list -> local_theory -> 
   14.18 +    (binding * mixfix -> typ -> term -> thm -> thm list -> Proof.context ->
   14.19 +      lift_def * local_theory) ->
   14.20 +    binding * mixfix -> typ -> term -> thm list -> local_theory ->
   14.21      term option * (thm -> Proof.context -> lift_def * local_theory)
   14.22  
   14.23    val gen_lift_def:
   14.24 -    (binding * mixfix -> typ -> term -> thm -> thm list -> local_theory -> 
   14.25 -      lift_def * local_theory) -> 
   14.26 -    binding * mixfix -> typ -> term -> (Proof.context -> tactic) -> thm list -> 
   14.27 +    (binding * mixfix -> typ -> term -> thm -> thm list -> local_theory ->
   14.28 +      lift_def * local_theory) ->
   14.29 +    binding * mixfix -> typ -> term -> (Proof.context -> tactic) -> thm list ->
   14.30      local_theory -> lift_def * local_theory
   14.31  
   14.32 -  val lift_def: 
   14.33 -    config -> binding * mixfix -> typ -> term -> (Proof.context -> tactic) -> thm list -> 
   14.34 +  val lift_def:
   14.35 +    config -> binding * mixfix -> typ -> term -> (Proof.context -> tactic) -> thm list ->
   14.36      local_theory -> lift_def * local_theory
   14.37  
   14.38    val can_generate_code_cert: thm -> bool
   14.39 @@ -89,7 +89,7 @@
   14.40  fun mk_lift_def rty qty rhs lift_const def_thm rsp_thm abs_eq rep_eq code_eq transfer_rules =
   14.41    LIFT_DEF {rty = rty, qty = qty,
   14.42              rhs = rhs, lift_const = lift_const,
   14.43 -            def_thm = def_thm, rsp_thm = rsp_thm, abs_eq = abs_eq, rep_eq = rep_eq, 
   14.44 +            def_thm = def_thm, rsp_thm = rsp_thm, abs_eq = abs_eq, rep_eq = rep_eq,
   14.45              code_eq = code_eq, transfer_rules = transfer_rules };
   14.46  
   14.47  fun map_lift_def f1 f2 f3 f4 f5 f6 f7 f8 f9 f10
   14.48 @@ -129,8 +129,8 @@
   14.49    let
   14.50      val refl_rules = Lifting_Info.get_reflexivity_rules ctxt
   14.51      val transfer_rules = Transfer.get_transfer_raw ctxt
   14.52 -    
   14.53 -    fun main_tac i = (REPEAT_ALL_NEW (DETERM o resolve_tac ctxt refl_rules) THEN_ALL_NEW 
   14.54 +
   14.55 +    fun main_tac i = (REPEAT_ALL_NEW (DETERM o resolve_tac ctxt refl_rules) THEN_ALL_NEW
   14.56        (REPEAT_ALL_NEW (DETERM o resolve_tac ctxt transfer_rules))) i
   14.57    in
   14.58      SOME (Goal.prove ctxt [] [] prop (K (main_tac 1)))
   14.59 @@ -143,7 +143,7 @@
   14.60        let
   14.61          val T = fastype_of x
   14.62        in
   14.63 -        Const (@{const_name "less_eq"}, T --> T --> HOLogic.boolT) $ 
   14.64 +        Const (@{const_name "less_eq"}, T --> T --> HOLogic.boolT) $
   14.65            (Const (@{const_name HOL.eq}, T)) $ x
   14.66        end;
   14.67      val goal = HOLogic.mk_Trueprop (mk_ge_eq rel);
   14.68 @@ -165,11 +165,11 @@
   14.69        | NONE => NONE
   14.70    end
   14.71  
   14.72 -(* 
   14.73 +(*
   14.74    Generates a parametrized transfer rule.
   14.75    transfer_rule - of the form T t f
   14.76    parametric_transfer_rule - of the form par_R t' t
   14.77 -  
   14.78 +
   14.79    Result: par_T t' f, after substituing op= for relations in par_R that relate
   14.80      a type constructor to the same type constructor, it is a merge of (par_R' OO T) t' f
   14.81      using Lifting_Term.merge_transfer_relations
   14.82 @@ -182,8 +182,8 @@
   14.83          val tm = (strip_args 2 o HOLogic.dest_Trueprop o Thm.concl_of) thm;
   14.84          val param_rel = (snd o dest_comb o fst o dest_comb) tm;
   14.85          val free_vars = Term.add_vars param_rel [];
   14.86 -        
   14.87 -        fun make_subst (xi, typ) subst = 
   14.88 +
   14.89 +        fun make_subst (xi, typ) subst =
   14.90            let
   14.91              val [rty, rty'] = binder_types typ
   14.92            in
   14.93 @@ -195,7 +195,7 @@
   14.94  
   14.95          val inst_thm = infer_instantiate ctxt (fold make_subst free_vars []) thm;
   14.96        in
   14.97 -        Conv.fconv_rule 
   14.98 +        Conv.fconv_rule
   14.99            ((Conv.concl_conv (Thm.nprems_of inst_thm) o
  14.100              HOLogic.Trueprop_conv o Conv.fun2_conv o Conv.arg1_conv)
  14.101              (Raw_Simplifier.rewrite ctxt false (Transfer.get_sym_relator_eq ctxt))) inst_thm
  14.102 @@ -227,7 +227,7 @@
  14.103        in
  14.104          [Lifting_Term.merge_transfer_relations ctxt goal, thm] MRSL @{thm POS_apply}
  14.105        end
  14.106 -     
  14.107 +
  14.108      val thm =
  14.109        inst_relcomppI ctxt parametric_transfer_rule transfer_rule
  14.110          OF [parametric_transfer_rule, transfer_rule]
  14.111 @@ -248,9 +248,9 @@
  14.112      zipped_thm
  14.113    end
  14.114  
  14.115 -fun print_generate_transfer_info msg = 
  14.116 +fun print_generate_transfer_info msg =
  14.117    let
  14.118 -    val error_msg = cat_lines 
  14.119 +    val error_msg = cat_lines
  14.120        ["Generation of a parametric transfer rule failed.",
  14.121        (Pretty.string_of (Pretty.block
  14.122           [Pretty.str "Reason:", Pretty.brk 2, msg]))]
  14.123 @@ -279,18 +279,18 @@
  14.124  fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W)
  14.125    | get_binder_types _ = []
  14.126  
  14.127 -fun get_binder_types_by_rel (Const (@{const_name "rel_fun"}, _) $ _ $ S) (Type ("fun", [T, U]), Type ("fun", [V, W])) = 
  14.128 +fun get_binder_types_by_rel (Const (@{const_name "rel_fun"}, _) $ _ $ S) (Type ("fun", [T, U]), Type ("fun", [V, W])) =
  14.129      (T, V) :: get_binder_types_by_rel S (U, W)
  14.130    | get_binder_types_by_rel _ _ = []
  14.131  
  14.132 -fun get_body_type_by_rel (Const (@{const_name "rel_fun"}, _) $ _ $ S) (Type ("fun", [_, U]), Type ("fun", [_, V])) = 
  14.133 +fun get_body_type_by_rel (Const (@{const_name "rel_fun"}, _) $ _ $ S) (Type ("fun", [_, U]), Type ("fun", [_, V])) =
  14.134      get_body_type_by_rel S (U, V)
  14.135    | get_body_type_by_rel _ (U, V)  = (U, V)
  14.136  
  14.137  fun get_binder_rels (Const (@{const_name "rel_fun"}, _) $ R $ S) = R :: get_binder_rels S
  14.138    | get_binder_rels _ = []
  14.139  
  14.140 -fun force_rty_type ctxt rty rhs = 
  14.141 +fun force_rty_type ctxt rty rhs =
  14.142    let
  14.143      val thy = Proof_Context.theory_of ctxt
  14.144      val rhs_schematic = singleton (Variable.polymorphic ctxt) rhs
  14.145 @@ -300,7 +300,7 @@
  14.146      Envir.subst_term_types match rhs_schematic
  14.147    end
  14.148  
  14.149 -fun unabs_def ctxt def = 
  14.150 +fun unabs_def ctxt def =
  14.151    let
  14.152      val (_, rhs) = Thm.dest_equals (Thm.cprop_of def)
  14.153      fun dest_abs (Abs (var_name, T, _)) = (var_name, T)
  14.154 @@ -313,15 +313,15 @@
  14.155      singleton (Proof_Context.export ctxt' ctxt)
  14.156    end
  14.157  
  14.158 -fun unabs_all_def ctxt def = 
  14.159 +fun unabs_all_def ctxt def =
  14.160    let
  14.161      val (_, rhs) = Thm.dest_equals (Thm.cprop_of def)
  14.162      val xs = strip_abs_vars (Thm.term_of rhs)
  14.163 -  in  
  14.164 +  in
  14.165      fold (K (unabs_def ctxt)) xs def
  14.166    end
  14.167  
  14.168 -val map_fun_unfolded = 
  14.169 +val map_fun_unfolded =
  14.170    @{thm map_fun_def[abs_def]} |>
  14.171    unabs_def @{context} |>
  14.172    unabs_def @{context} |>
  14.173 @@ -331,7 +331,7 @@
  14.174    let
  14.175      fun unfold_conv ctm =
  14.176        case (Thm.term_of ctm) of
  14.177 -        Const (@{const_name "map_fun"}, _) $ _ $ _ => 
  14.178 +        Const (@{const_name "map_fun"}, _) $ _ $ _ =>
  14.179            (Conv.arg_conv unfold_conv then_conv Conv.rewr_conv map_fun_unfolded) ctm
  14.180          | _ => Conv.all_conv ctm
  14.181    in
  14.182 @@ -340,14 +340,14 @@
  14.183  
  14.184  fun unfold_fun_maps_beta ctm =
  14.185    let val try_beta_conv = Conv.try_conv (Thm.beta_conversion false)
  14.186 -  in 
  14.187 -    (unfold_fun_maps then_conv try_beta_conv) ctm 
  14.188 +  in
  14.189 +    (unfold_fun_maps then_conv try_beta_conv) ctm
  14.190    end
  14.191  
  14.192  fun prove_rel ctxt rsp_thm (rty, qty) =
  14.193    let
  14.194      val ty_args = get_binder_types (rty, qty)
  14.195 -    fun disch_arg args_ty thm = 
  14.196 +    fun disch_arg args_ty thm =
  14.197        let
  14.198          val quot_thm = Lifting_Term.prove_quot_thm ctxt args_ty
  14.199        in
  14.200 @@ -359,7 +359,7 @@
  14.201  
  14.202  exception CODE_CERT_GEN of string
  14.203  
  14.204 -fun simplify_code_eq ctxt def_thm = 
  14.205 +fun simplify_code_eq ctxt def_thm =
  14.206    Local_Defs.unfold0 ctxt [@{thm o_apply}, @{thm map_fun_def}, @{thm id_apply}] def_thm
  14.207  
  14.208  (*
  14.209 @@ -378,10 +378,10 @@
  14.210    let
  14.211      val unfolded_def = Conv.fconv_rule (Conv.arg_conv unfold_fun_maps_beta) def_thm
  14.212      val unabs_def = unabs_all_def ctxt unfolded_def
  14.213 -  in  
  14.214 -    if body_type rty = body_type qty then 
  14.215 +  in
  14.216 +    if body_type rty = body_type qty then
  14.217        SOME (simplify_code_eq ctxt (unabs_def RS @{thm meta_eq_to_obj_eq}))
  14.218 -    else 
  14.219 +    else
  14.220        let
  14.221          val quot_thm = Lifting_Term.prove_quot_thm ctxt (get_body_types (rty, qty))
  14.222          val rel_fun = prove_rel ctxt rsp_thm (rty, qty)
  14.223 @@ -411,8 +411,8 @@
  14.224          val ty_args = get_binder_types_by_rel rel (rty, qty)
  14.225          val body_type = get_body_type_by_rel rel (rty, qty)
  14.226          val quot_ret_thm = Lifting_Term.prove_quot_thm ctxt body_type
  14.227 -        
  14.228 -        val rep_abs_folded_unmapped_thm = 
  14.229 +
  14.230 +        val rep_abs_folded_unmapped_thm =
  14.231            let
  14.232              val rep_id = [quot_thm, def_thm] MRSL @{thm Quotient_Rep_eq}
  14.233              val ctm = Thm.dest_equals_lhs (Thm.cprop_of rep_id)
  14.234 @@ -428,10 +428,10 @@
  14.235          |> fold (fn _ => fn thm => thm RS @{thm rel_funD2}) ty_args
  14.236          |> (fn x => x RS (@{thm Quotient_rel_abs2} OF [quot_ret_thm]))
  14.237        end
  14.238 -    
  14.239 +
  14.240      val prem_rels = get_binder_rels (quot_thm_rel quot_thm);
  14.241 -    val proved_assms = prem_rels |> map (try_prove_refl_rel ctxt) 
  14.242 -      |> map_index (apfst (fn x => x + 1)) |> filter (is_some o snd) |> map (apsnd the) 
  14.243 +    val proved_assms = prem_rels |> map (try_prove_refl_rel ctxt)
  14.244 +      |> map_index (apfst (fn x => x + 1)) |> filter (is_some o snd) |> map (apsnd the)
  14.245        |> map (apsnd (fn assm => assm RS @{thm ge_eq_refl}))
  14.246      val abs_eq = fold_rev (fn (i, assm) => fn thm => assm RSN (i, thm)) proved_assms abs_eq_with_assms
  14.247    in
  14.248 @@ -445,7 +445,7 @@
  14.249        | no_abstr (Abs (_, _, t)) = no_abstr t
  14.250        | no_abstr (Const (name, _)) = not (Code.is_abstr thy name)
  14.251        | no_abstr _ = true
  14.252 -    fun is_valid_eq eqn = can (Code.assert_eqn thy) (mk_meta_eq eqn, true) 
  14.253 +    fun is_valid_eq eqn = can (Code.assert_eqn thy) (mk_meta_eq eqn, true)
  14.254        andalso no_abstr (Thm.prop_of eqn)
  14.255      fun is_valid_abs_eq abs_eq = can (Code.assert_abs_eqn thy NONE) (mk_meta_eq abs_eq)
  14.256  
  14.257 @@ -474,8 +474,8 @@
  14.258      else
  14.259        if is_Type qty then
  14.260          if Lifting_Info.is_no_code_type ctxt (Tname qty) then false
  14.261 -        else 
  14.262 -          let 
  14.263 +        else
  14.264 +          let
  14.265              val (rty', rtyq) = Lifting_Term.instantiate_rtys ctxt (rty, qty)
  14.266              val (rty's, rtyqs) = (Targs rty', Targs rtyq)
  14.267            in
  14.268 @@ -484,26 +484,26 @@
  14.269        else
  14.270          true
  14.271  
  14.272 -  fun encode_code_eq ctxt abs_eq opt_rep_eq (rty, qty) = 
  14.273 +  fun encode_code_eq ctxt abs_eq opt_rep_eq (rty, qty) =
  14.274      let
  14.275        fun mk_type typ = typ |> Logic.mk_type |> Thm.cterm_of ctxt |> Drule.mk_term
  14.276      in
  14.277        Conjunction.intr_balanced [abs_eq, (the_default TrueI opt_rep_eq), mk_type rty, mk_type qty]
  14.278      end
  14.279 -  
  14.280 +
  14.281    exception DECODE
  14.282 -    
  14.283 +
  14.284    fun decode_code_eq thm =
  14.285 -    if Thm.nprems_of thm > 0 then raise DECODE 
  14.286 +    if Thm.nprems_of thm > 0 then raise DECODE
  14.287      else
  14.288        let
  14.289          val [abs_eq, rep_eq, rty, qty] = Conjunction.elim_balanced 4 thm
  14.290          val opt_rep_eq = if Thm.eq_thm_prop (rep_eq, TrueI) then NONE else SOME rep_eq
  14.291          fun dest_type typ = typ |> Drule.dest_term |> Thm.term_of |> Logic.dest_type
  14.292        in
  14.293 -        (abs_eq, opt_rep_eq, (dest_type rty, dest_type qty)) 
  14.294 +        (abs_eq, opt_rep_eq, (dest_type rty, dest_type qty))
  14.295        end
  14.296 -  
  14.297 +
  14.298    structure Data = Generic_Data
  14.299    (
  14.300      type T = code_eq option
  14.301 @@ -520,7 +520,7 @@
  14.302        Context.theory_map (Data.put (SOME code_eq)) thy
  14.303      end
  14.304      handle DECODE => thy
  14.305 -  
  14.306 +
  14.307    val register_code_eq_attribute = Thm.declaration_attribute
  14.308      (fn thm => Context.mapping (register_encoded_code_eq thm) I)
  14.309    val register_code_eq_attrib = Attrib.internal (K register_code_eq_attribute)
  14.310 @@ -533,14 +533,15 @@
  14.311    in
  14.312      if no_no_code lthy (rty, qty) then
  14.313        let
  14.314 -        val lthy = (snd oo Local_Theory.note) 
  14.315 +        val lthy = (snd oo Local_Theory.note)
  14.316            ((Binding.empty, [register_code_eq_attrib]), [encoded_code_eq]) lthy
  14.317          val opt_code_eq = Data.get (Context.Theory (Proof_Context.theory_of lthy))
  14.318 -        val code_eq = if is_some opt_code_eq then the opt_code_eq 
  14.319 +        val code_eq =
  14.320 +          if is_some opt_code_eq then the opt_code_eq
  14.321            else UNKNOWN_EQ (* UNKNOWN_EQ means that we are in a locale and we do not know
  14.322              which code equation is going to be used. This is going to be resolved at the
  14.323              point when an interpretation of the locale is executed. *)
  14.324 -        val lthy = Local_Theory.declaration {syntax = false, pervasive = true} 
  14.325 +        val lthy = Local_Theory.declaration {syntax = false, pervasive = true}
  14.326            (K (Data.put NONE)) lthy
  14.327        in
  14.328          (code_eq, lthy)
  14.329 @@ -549,9 +550,9 @@
  14.330        (NONE_EQ, lthy)
  14.331    end
  14.332  end
  14.333 -            
  14.334 +
  14.335  (*
  14.336 -  Defines an operation on an abstract type in terms of a corresponding operation 
  14.337 +  Defines an operation on an abstract type in terms of a corresponding operation
  14.338      on a representation type.
  14.339  
  14.340    var - a binding and a mixfix of the new constant being defined
  14.341 @@ -575,8 +576,8 @@
  14.342      val (_, newrhs) = Local_Defs.abs_def prop'
  14.343      val var = ((#notes config = false ? Binding.concealed) binding, mx)
  14.344      val def_name = Thm.make_def_binding (#notes config) (#1 var)
  14.345 -    
  14.346 -    val ((lift_const, (_ , def_thm)), lthy) = 
  14.347 +
  14.348 +    val ((lift_const, (_ , def_thm)), lthy) =
  14.349        Local_Theory.define (var, ((def_name, []), newrhs)) lthy
  14.350  
  14.351      val transfer_rules = generate_transfer_rules lthy quot_thm rsp_thm def_thm par_thms
  14.352 @@ -591,18 +592,18 @@
  14.353          val abs_eq_thmN = Binding.qualify_name true lhs_name "abs_eq"
  14.354          val rep_eq_thmN = Binding.qualify_name true lhs_name "rep_eq"
  14.355          val transfer_ruleN = Binding.qualify_name true lhs_name "transfer"
  14.356 -        val notes = 
  14.357 -          [(rsp_thmN, [], [rsp_thm]), 
  14.358 +        val notes =
  14.359 +          [(rsp_thmN, [], [rsp_thm]),
  14.360            (transfer_ruleN, @{attributes [transfer_rule]}, transfer_rules),
  14.361 -          (abs_eq_thmN, [], [abs_eq_thm])] 
  14.362 +          (abs_eq_thmN, [], [abs_eq_thm])]
  14.363            @ (case opt_rep_eq_thm of SOME rep_eq_thm => [(rep_eq_thmN, [], [rep_eq_thm])] | NONE => [])
  14.364        in
  14.365          if names then map (fn (name, attrs, thms) => ((name, []), [(thms, attrs)])) notes
  14.366 -        else map_filter (fn (_, attrs, thms) => if null attrs then NONE 
  14.367 -          else SOME ((Binding.empty, []), [(thms, attrs)])) notes
  14.368 +        else map_filter (fn (_, attrs, thms) => if null attrs then NONE
  14.369 +          else SOME (Binding.empty_atts, [(thms, attrs)])) notes
  14.370        end
  14.371      val (code_eq, lthy) = register_code_eq abs_eq_thm opt_rep_eq_thm (rty_forced, qty) lthy
  14.372 -    val lift_def = mk_lift_def rty_forced qty newrhs lift_const def_thm rsp_thm abs_eq_thm 
  14.373 +    val lift_def = mk_lift_def rty_forced qty newrhs lift_const def_thm rsp_thm abs_eq_thm
  14.374            opt_rep_eq_thm code_eq transfer_rules
  14.375    in
  14.376      lthy
  14.377 @@ -616,8 +617,8 @@
  14.378  fun get_cr_pcr_eqs ctxt =
  14.379    let
  14.380      fun collect (data : Lifting_Info.quotient) l =
  14.381 -      if is_some (#pcr_info data) 
  14.382 -      then ((Thm.symmetric o safe_mk_meta_eq o #pcr_cr_eq o the o #pcr_info) data :: l) 
  14.383 +      if is_some (#pcr_info data)
  14.384 +      then ((Thm.symmetric o safe_mk_meta_eq o #pcr_cr_eq o the o #pcr_info) data :: l)
  14.385        else l
  14.386      val table = Lifting_Info.get_quotients ctxt
  14.387    in
  14.388 @@ -629,7 +630,7 @@
  14.389      val rsp_rel = Lifting_Term.equiv_relation lthy (fastype_of rhs, qty)
  14.390      val rty_forced = (domain_type o fastype_of) rsp_rel;
  14.391      val forced_rhs = force_rty_type lthy rty_forced rhs;
  14.392 -    val cr_to_pcr_conv = HOLogic.Trueprop_conv (Conv.fun2_conv 
  14.393 +    val cr_to_pcr_conv = HOLogic.Trueprop_conv (Conv.fun2_conv
  14.394        (Raw_Simplifier.rewrite lthy false (get_cr_pcr_eqs lthy)))
  14.395      val (prsp_tm, rsp_prsp_eq) = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs)
  14.396        |> Thm.cterm_of lthy
  14.397 @@ -639,13 +640,13 @@
  14.398        |>> snd
  14.399      val to_rsp = rsp_prsp_eq RS Drule.equal_elim_rule2
  14.400      val opt_proven_rsp_thm = try_prove_reflexivity lthy prsp_tm
  14.401 -    
  14.402 -    fun after_qed internal_rsp_thm lthy = 
  14.403 +
  14.404 +    fun after_qed internal_rsp_thm lthy =
  14.405        add_lift_def var qty rhs (internal_rsp_thm RS to_rsp) par_thms lthy
  14.406    in
  14.407      case opt_proven_rsp_thm of
  14.408        SOME thm => (NONE, K (after_qed thm))
  14.409 -      | NONE => (SOME prsp_tm, after_qed) 
  14.410 +      | NONE => (SOME prsp_tm, after_qed)
  14.411    end
  14.412  
  14.413  fun gen_lift_def add_lift_def var qty rhs tac par_thms lthy =
  14.414 @@ -653,8 +654,8 @@
  14.415      val (goal, after_qed) = prepare_lift_def add_lift_def var qty rhs par_thms lthy
  14.416    in
  14.417      case goal of
  14.418 -      SOME goal => 
  14.419 -        let 
  14.420 +      SOME goal =>
  14.421 +        let
  14.422            val rsp_thm = Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => tac ctxt)
  14.423              |> Thm.close_derivation
  14.424          in
    15.1 --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Wed Jun 22 16:04:03 2016 +0200
    15.2 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Thu Jun 23 11:01:14 2016 +0200
    15.3 @@ -298,8 +298,9 @@
    15.4                EVERY' [Transfer.gen_frees_tac [] ctxt, DETERM o Transfer.transfer_tac true ctxt,
    15.5                  SELECT_GOAL (Local_Defs.unfold0_tac ctxt [id_apply]), rtac ctxt refl] i;
    15.6              val rep_isom_transfer = transfer_of_rep_isom_data rep_isom_data
    15.7 -            val (_, transfer_lthy) = Proof_Context.note_thmss "" [((Binding.empty, []),
    15.8 -              [([rep_isom_transfer], [Transfer.transfer_add])])] lthy
    15.9 +            val (_, transfer_lthy) =
   15.10 +              Proof_Context.note_thmss ""
   15.11 +                [(Binding.empty_atts, [([rep_isom_transfer], [Transfer.transfer_add])])] lthy
   15.12              val f_alt_def = Goal.prove_sorry transfer_lthy [] [] f_alt_def_goal
   15.13                (fn {context = ctxt, prems = _} => HEADGOAL (f_alt_def_tac ctxt))
   15.14                |> Thm.close_derivation
   15.15 @@ -444,9 +445,10 @@
   15.16            (map safe_mk_meta_eq @{thms id_apply simp_thms Ball_def}),
   15.17           rtac ctxt TrueI] i;
   15.18  
   15.19 -    val (_, transfer_lthy) = Proof_Context.note_thmss "" [((Binding.empty, []),
   15.20 -      [(@{thms right_total_UNIV_transfer},[Transfer.transfer_add]),
   15.21 -       (@{thms Domain_eq_top}, [Transfer.transfer_domain_add]) ])] lthy;
   15.22 +    val (_, transfer_lthy) =
   15.23 +      Proof_Context.note_thmss "" [(Binding.empty_atts,
   15.24 +        [(@{thms right_total_UNIV_transfer},[Transfer.transfer_add]),
   15.25 +         (@{thms Domain_eq_top}, [Transfer.transfer_domain_add])])] lthy;
   15.26  
   15.27      val quot_thm_isom = Goal.prove_sorry transfer_lthy [] [] typedef_goal
   15.28        (fn {context = ctxt, prems = _} => typ_isom_tac ctxt 1)
    16.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Jun 22 16:04:03 2016 +0200
    16.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Jun 23 11:01:14 2016 +0200
    16.3 @@ -45,10 +45,13 @@
    16.4      val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
    16.5      val crel_name = Binding.prefix_name "cr_" qty_name
    16.6      val (fixed_def_term, lthy) = yield_singleton (Variable.importT_terms) def_term lthy
    16.7 -    val ((_, (_ , def_thm)), lthy) = if #notes config then
    16.8 -        Local_Theory.define ((crel_name, NoSyn), ((Thm.def_binding crel_name, []), fixed_def_term)) lthy
    16.9 +    val ((_, (_ , def_thm)), lthy) =
   16.10 +      if #notes config then
   16.11 +        Local_Theory.define
   16.12 +          ((crel_name, NoSyn), ((Thm.def_binding crel_name, []), fixed_def_term)) lthy
   16.13        else 
   16.14 -        Local_Theory.define ((Binding.concealed crel_name, NoSyn), ((Binding.empty, []), fixed_def_term)) lthy
   16.15 +        Local_Theory.define
   16.16 +          ((Binding.concealed crel_name, NoSyn), (Binding.empty_atts, fixed_def_term)) lthy
   16.17    in  
   16.18      (def_thm, lthy)
   16.19    end
   16.20 @@ -90,12 +93,13 @@
   16.21      val definition_term = Logic.mk_equals (lhs, rhs)
   16.22      fun note_def lthy =
   16.23        Specification.definition (SOME (pcrel_name, SOME relator_type, NoSyn)) [] []
   16.24 -        ((Binding.empty, []), definition_term) lthy |>> (snd #> snd);
   16.25 +        (Binding.empty_atts, definition_term) lthy |>> (snd #> snd);
   16.26      fun raw_def lthy =
   16.27        let
   16.28          val ((_, rhs), prove) = Local_Defs.derived_def lthy {conditional = true} definition_term;
   16.29 -        val ((_, (_, raw_th)), lthy) = lthy
   16.30 -          |> Local_Theory.define ((Binding.concealed pcrel_name, NoSyn), ((Binding.empty, []), rhs));
   16.31 +        val ((_, (_, raw_th)), lthy) =
   16.32 +          Local_Theory.define
   16.33 +            ((Binding.concealed pcrel_name, NoSyn), (Binding.empty_atts, rhs)) lthy;
   16.34          val th = prove lthy raw_th;
   16.35        in
   16.36          (th, lthy)
   16.37 @@ -498,9 +502,9 @@
   16.38  fun notes names thms = 
   16.39    let
   16.40      val notes =
   16.41 -        if names then map (fn (name, thms, attrs) => ((name, []), [(thms, attrs)])) thms
   16.42 -        else map_filter (fn (_, thms, attrs) => if null attrs then NONE 
   16.43 -          else SOME ((Binding.empty, []), [(thms, attrs)])) thms
   16.44 +      if names then map (fn (name, thms, attrs) => ((name, []), [(thms, attrs)])) thms
   16.45 +      else map_filter (fn (_, thms, attrs) => if null attrs then NONE 
   16.46 +        else SOME (Binding.empty_atts, [(thms, attrs)])) thms
   16.47    in
   16.48      Local_Theory.notes notes #> snd
   16.49    end
    17.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Wed Jun 22 16:04:03 2016 +0200
    17.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Thu Jun 23 11:01:14 2016 +0200
    17.3 @@ -177,7 +177,7 @@
    17.4            {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
    17.5             coind = false, no_elim = true, no_ind = false, skip_mono = true}
    17.6            (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
    17.7 -          (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
    17.8 +          (map (fn x => (Binding.empty_atts, x)) intr_ts) []
    17.9        ||> Sign.restore_naming thy1;
   17.10  
   17.11      (********************************* typedef ********************************)
    18.1 --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Wed Jun 22 16:04:03 2016 +0200
    18.2 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Thu Jun 23 11:01:14 2016 +0200
    18.3 @@ -155,7 +155,7 @@
    18.4              coind = false, no_elim = false, no_ind = true, skip_mono = true}
    18.5            (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    18.6            (map dest_Free rec_fns)
    18.7 -          (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
    18.8 +          (map (fn x => (Binding.empty_atts, x)) rec_intr_ts) []
    18.9        ||> Sign.restore_naming thy0;
   18.10  
   18.11      (* prove uniqueness and termination of primrec combinators *)
    19.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Jun 22 16:04:03 2016 +0200
    19.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Jun 23 11:01:14 2016 +0200
    19.3 @@ -374,7 +374,7 @@
    19.4    else
    19.5      fold_map (fn (name, T) => Local_Theory.define
    19.6          ((Binding.concealed (Binding.name name), NoSyn),
    19.7 -          (apfst Binding.concealed Attrib.empty_binding, mk_undefined T))
    19.8 +          (apfst Binding.concealed Binding.empty_atts, mk_undefined T))
    19.9        #> apfst fst) (names ~~ Ts)
   19.10      #> (fn (consts, lthy) =>
   19.11        let
    20.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Jun 22 16:04:03 2016 +0200
    20.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Jun 23 11:01:14 2016 +0200
    20.3 @@ -141,7 +141,7 @@
    20.4          val proj_eqs = map2 (fn v => fn proj => (v, lambda arg proj)) vs projs;
    20.5          val proj_defs = map2 (fn Free (name, _) => fn (_, rhs) =>
    20.6            ((Binding.concealed (Binding.name name), NoSyn),
    20.7 -            (apfst Binding.concealed Attrib.empty_binding, rhs))) vs proj_eqs;
    20.8 +            (apfst Binding.concealed Binding.empty_atts, rhs))) vs proj_eqs;
    20.9          val aux_eq' = Pattern.rewrite_term thy proj_eqs [] aux_eq;
   20.10          fun prove_eqs aux_simp proj_defs lthy = 
   20.11            let
    21.1 --- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Wed Jun 22 16:04:03 2016 +0200
    21.2 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Thu Jun 23 11:01:14 2016 +0200
    21.3 @@ -133,7 +133,7 @@
    21.4  (* relator_eq *)
    21.5  
    21.6  fun relator_eq bnf =
    21.7 -  [((Binding.empty, []), [([rel_eq_of_bnf bnf], @{attributes [relator_eq]})])]
    21.8 +  [(Binding.empty_atts, [([rel_eq_of_bnf bnf], @{attributes [relator_eq]})])]
    21.9  
   21.10  (* transfer rules *)
   21.11  
   21.12 @@ -143,7 +143,7 @@
   21.13        :: rel_transfer_of_bnf bnf :: set_transfer_of_bnf bnf
   21.14      val transfer_attr = @{attributes [transfer_rule]}
   21.15    in
   21.16 -    map (fn thm => ((Binding.empty,[]),[([thm],transfer_attr)])) transfer_rules
   21.17 +    map (fn thm => (Binding.empty_atts, [([thm],transfer_attr)])) transfer_rules
   21.18    end
   21.19  
   21.20  (* Domainp theorem for predicator *)
   21.21 @@ -251,7 +251,7 @@
   21.22        @ (#co_rec_transfers o #fp_co_induct_sugar) fp_sugar
   21.23      val transfer_attr = @{attributes [transfer_rule]}
   21.24    in
   21.25 -    map (fn thm => ((Binding.empty, []), [([thm], transfer_attr)])) transfer_rules
   21.26 +    map (fn thm => (Binding.empty_atts, [([thm], transfer_attr)])) transfer_rules
   21.27    end
   21.28  
   21.29  fun register_pred_injects fp_sugar lthy =
    22.1 --- a/src/HOL/Tools/record.ML	Wed Jun 22 16:04:03 2016 +0200
    22.2 +++ b/src/HOL/Tools/record.ML	Thu Jun 23 11:01:14 2016 +0200
    22.3 @@ -1781,7 +1781,7 @@
    22.4        |> fold (Code.add_eqn (Code.Equation, true)) simps
    22.5        |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
    22.6        |> `(fn lthy => Syntax.check_term lthy eq)
    22.7 -      |-> (fn eq => Specification.definition NONE [] [] (Attrib.empty_binding, eq))
    22.8 +      |-> (fn eq => Specification.definition NONE [] [] (Binding.empty_atts, eq))
    22.9        |-> (fn (_, (_, eq_def)) =>
   22.10           Class.prove_instantiation_exit_result Morphism.thm tac eq_def)
   22.11        |-> (fn eq_def => fn thy =>
    23.1 --- a/src/HOL/Typerep.thy	Wed Jun 22 16:04:03 2016 +0200
    23.2 +++ b/src/HOL/Typerep.thy	Thu Jun 23 11:01:14 2016 +0200
    23.3 @@ -58,7 +58,7 @@
    23.4      thy
    23.5      |> Class.instantiation ([tyco], vs, @{sort typerep})
    23.6      |> `(fn lthy => Syntax.check_term lthy eq)
    23.7 -    |-> (fn eq => Specification.definition NONE [] [] (Attrib.empty_binding, eq))
    23.8 +    |-> (fn eq => Specification.definition NONE [] [] (Binding.empty_atts, eq))
    23.9      |> snd
   23.10      |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   23.11    end;
    24.1 --- a/src/Pure/General/binding.ML	Wed Jun 22 16:04:03 2016 +0200
    24.2 +++ b/src/Pure/General/binding.ML	Thu Jun 23 11:01:14 2016 +0200
    24.3 @@ -25,6 +25,8 @@
    24.4    val eq_name: binding * binding -> bool
    24.5    val empty: binding
    24.6    val is_empty: binding -> bool
    24.7 +  val empty_atts: binding * 'a list
    24.8 +  val is_empty_atts: binding * 'a list -> bool
    24.9    val conglomerate: binding list -> binding
   24.10    val qualify: bool -> string -> binding -> binding
   24.11    val qualify_name: bool -> binding -> string -> binding
   24.12 @@ -102,6 +104,9 @@
   24.13  val empty = name "";
   24.14  fun is_empty b = name_of b = "";
   24.15  
   24.16 +val empty_atts = (empty, []);
   24.17 +fun is_empty_atts (b, atts) = is_empty b andalso null atts;
   24.18 +
   24.19  fun conglomerate [b] = b
   24.20    | conglomerate bs = name (space_implode "_" (map name_of bs));
   24.21  
    25.1 --- a/src/Pure/Isar/attrib.ML	Wed Jun 22 16:04:03 2016 +0200
    25.2 +++ b/src/Pure/Isar/attrib.ML	Thu Jun 23 11:01:14 2016 +0200
    25.3 @@ -6,8 +6,6 @@
    25.4  
    25.5  signature ATTRIB =
    25.6  sig
    25.7 -  val empty_binding: Attrib.binding
    25.8 -  val is_empty_binding: Attrib.binding -> bool
    25.9    val print_attributes: bool -> Proof.context -> unit
   25.10    val define_global: binding -> (Token.src -> attribute) -> string -> theory -> string * theory
   25.11    val define: binding -> (Token.src -> attribute) -> string -> local_theory -> string * local_theory
   25.12 @@ -80,13 +78,8 @@
   25.13  structure Attrib: sig type binding = Attrib.binding include ATTRIB end =
   25.14  struct
   25.15  
   25.16 -(* source and bindings *)
   25.17 -
   25.18  type binding = Attrib.binding;
   25.19  
   25.20 -val empty_binding: binding = (Binding.empty, []);
   25.21 -fun is_empty_binding ((b, srcs): binding) = Binding.is_empty b andalso null srcs;
   25.22 -
   25.23  
   25.24  
   25.25  (** named attributes **)
   25.26 @@ -199,8 +192,8 @@
   25.27  
   25.28  fun eval_thms ctxt srcs = ctxt
   25.29    |> Proof_Context.note_thmss ""
   25.30 -    (map_facts_refs (map (attribute_cmd ctxt)) (Proof_Context.get_fact ctxt)
   25.31 -      [((Binding.empty, []), srcs)])
   25.32 +    (map_facts_refs
   25.33 +      (map (attribute_cmd ctxt)) (Proof_Context.get_fact ctxt) [(Binding.empty_atts, srcs)])
   25.34    |> fst |> maps snd;
   25.35  
   25.36  
   25.37 @@ -362,10 +355,10 @@
   25.38            if eq_list (eq_fst Thm.eq_thm_strict) (decls', fact') then
   25.39              [((b, []), map2 (fn (th, atts1) => fn (_, atts2) => (th, atts1 @ atts2)) decls' fact')]
   25.40            else if null decls' then [((b, []), fact')]
   25.41 -          else [(empty_binding, decls'), ((b, []), fact')];
   25.42 +          else [(Binding.empty_atts, decls'), ((b, []), fact')];
   25.43        in (facts', context') end)
   25.44    |> fst |> flat |> map (apsnd (map (apfst single)))
   25.45 -  |> filter_out (fn (b, fact) => is_empty_binding b andalso forall (null o #2) fact);
   25.46 +  |> filter_out (fn (b, fact) => Binding.is_empty_atts b andalso forall (null o #2) fact);
   25.47  
   25.48  end;
   25.49  
    26.1 --- a/src/Pure/Isar/bundle.ML	Wed Jun 22 16:04:03 2016 +0200
    26.2 +++ b/src/Pure/Isar/bundle.ML	Thu Jun 23 11:01:14 2016 +0200
    26.3 @@ -112,7 +112,7 @@
    26.4      val bundle0 = raw_bundle
    26.5        |> map (fn (fact, atts) => (prep_fact ctxt' fact, map (prep_att ctxt') atts));
    26.6      val bundle =
    26.7 -      Attrib.partial_evaluation ctxt' [(Attrib.empty_binding, bundle0)] |> map snd |> flat
    26.8 +      Attrib.partial_evaluation ctxt' [(Binding.empty_atts, bundle0)] |> map snd |> flat
    26.9        |> transform_bundle (Proof_Context.export_morphism ctxt' lthy);
   26.10    in
   26.11      lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
   26.12 @@ -200,7 +200,7 @@
   26.13    let val decls = maps (get ctxt) args in
   26.14      ctxt
   26.15      |> Context_Position.set_visible false
   26.16 -    |> notes [((Binding.empty, []), decls)] |> #2
   26.17 +    |> notes [(Binding.empty_atts, decls)] |> #2
   26.18      |> Context_Position.restore_visible ctxt
   26.19    end;
   26.20  
    27.1 --- a/src/Pure/Isar/class_declaration.ML	Wed Jun 22 16:04:03 2016 +0200
    27.2 +++ b/src/Pure/Isar/class_declaration.ML	Thu Jun 23 11:01:14 2016 +0200
    27.3 @@ -298,14 +298,14 @@
    27.4        | [thm] => SOME thm);
    27.5    in
    27.6      thy
    27.7 -    |> add_consts class base_sort sups supparam_names global_syntax
    27.8 -    |-> (fn (param_map, params) => Axclass.define_class (bname, supsort)
    27.9 -          (map (fst o snd) params)
   27.10 -          [(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)]
   27.11 -    #> snd
   27.12 -    #> `get_axiom
   27.13 -    #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
   27.14 -    #> pair (param_map, params, assm_axiom)))
   27.15 +    |> add_consts class base_sort sups supparam_names global_syntax |-> (fn (param_map, params) =>
   27.16 +      Axclass.define_class (bname, supsort)
   27.17 +        (map (fst o snd) params)
   27.18 +          [(Binding.empty_atts, Option.map (globalize param_map) raw_pred |> the_list)]
   27.19 +      #> snd
   27.20 +      #> `get_axiom
   27.21 +      #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
   27.22 +      #> pair (param_map, params, assm_axiom)))
   27.23    end;
   27.24  
   27.25  fun gen_class prep_class_spec b raw_supclasses raw_elems thy =
    28.1 --- a/src/Pure/Isar/element.ML	Wed Jun 22 16:04:03 2016 +0200
    28.2 +++ b/src/Pure/Isar/element.ML	Thu Jun 23 11:01:14 2016 +0200
    28.3 @@ -239,8 +239,8 @@
    28.4          then insert (op =) (Variable.revert_fixed ctxt' x, T) else I | _ => I) prop []);
    28.5    in
    28.6      pretty_ctxt ctxt' (Fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) fixes)) @
    28.7 -    pretty_ctxt ctxt' (Assumes (map (fn t => (Attrib.empty_binding, [(t, [])])) assumes)) @
    28.8 -     (if null cases then pretty_stmt ctxt' (Shows [(Attrib.empty_binding, [(concl, [])])])
    28.9 +    pretty_ctxt ctxt' (Assumes (map (fn t => (Binding.empty_atts, [(t, [])])) assumes)) @
   28.10 +     (if null cases then pretty_stmt ctxt' (Shows [(Binding.empty_atts, [(concl, [])])])
   28.11        else
   28.12          let val (clauses, ctxt'') = fold_map obtain cases ctxt'
   28.13          in pretty_stmt ctxt'' (Obtains clauses) end)
   28.14 @@ -293,7 +293,7 @@
   28.15    in
   28.16      Proof.map_context (K goal_ctxt) #>
   28.17      Proof.internal_goal (K (K ())) (Proof_Context.get_mode goal_ctxt) true cmd
   28.18 -      NONE after_qed' [] [] (map (pair Thm.empty_binding) propp) #> snd
   28.19 +      NONE after_qed' [] [] (map (pair Binding.empty_atts) propp) #> snd
   28.20    end;
   28.21  
   28.22  in
    29.1 --- a/src/Pure/Isar/expression.ML	Wed Jun 22 16:04:03 2016 +0200
    29.2 +++ b/src/Pure/Isar/expression.ML	Thu Jun 23 11:01:14 2016 +0200
    29.3 @@ -591,10 +591,10 @@
    29.4      val text' =
    29.5        text |>
    29.6         (if is_some asm then
    29.7 -          eval_text ctxt false (Assumes [(Attrib.empty_binding, [(the asm', [])])])
    29.8 +          eval_text ctxt false (Assumes [(Binding.empty_atts, [(the asm', [])])])
    29.9          else I) |>
   29.10         (if not (null defs) then
   29.11 -          eval_text ctxt false (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs'))
   29.12 +          eval_text ctxt false (Defines (map (fn def => (Binding.empty_atts, (def, []))) defs'))
   29.13          else I)
   29.14  (* FIXME clone from locale.ML *)
   29.15    in text' end;
    30.1 --- a/src/Pure/Isar/generic_target.ML	Wed Jun 22 16:04:03 2016 +0200
    30.2 +++ b/src/Pure/Isar/generic_target.ML	Thu Jun 23 11:01:14 2016 +0200
    30.3 @@ -243,7 +243,7 @@
    30.4      (*local definition*)
    30.5      val ([(lhs, (_, local_def))], lthy3) = lthy2
    30.6        |> Context_Position.set_visible false
    30.7 -      |> Local_Defs.define [((b, NoSyn), (Thm.empty_binding, lhs'))]
    30.8 +      |> Local_Defs.define [((b, NoSyn), (Binding.empty_atts, lhs'))]
    30.9        ||> Context_Position.restore_visible lthy2;
   30.10  
   30.11      (*result*)
    31.1 --- a/src/Pure/Isar/interpretation.ML	Wed Jun 22 16:04:03 2016 +0200
    31.2 +++ b/src/Pure/Isar/interpretation.ML	Thu Jun 23 11:01:14 2016 +0200
    31.3 @@ -120,7 +120,7 @@
    31.4  
    31.5  fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt =
    31.6    let
    31.7 -    val facts = (Attrib.empty_binding, [(map (Morphism.thm (export' $> export)) def_eqns, [])])
    31.8 +    val facts = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])])
    31.9        :: map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
   31.10      val (eqns', ctxt') = ctxt
   31.11        |> note Thm.theoremK facts
    32.1 --- a/src/Pure/Isar/locale.ML	Wed Jun 22 16:04:03 2016 +0200
    32.2 +++ b/src/Pure/Isar/locale.ML	Thu Jun 23 11:01:14 2016 +0200
    32.3 @@ -437,9 +437,9 @@
    32.4        (not (null params) ?
    32.5          activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
    32.6        (* FIXME type parameters *)
    32.7 -      (case asm of SOME A => activ_elem (Assumes [(Attrib.empty_binding, [(A, [])])]) | _ => I) |>
    32.8 +      (case asm of SOME A => activ_elem (Assumes [(Binding.empty_atts, [(A, [])])]) | _ => I) |>
    32.9        (not (null defs) ?
   32.10 -        activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs)));
   32.11 +        activ_elem (Defines (map (fn def => (Binding.empty_atts, (def, []))) defs)));
   32.12      val activate = activate_notes activ_elem transfer (Context.Theory thy) NONE;
   32.13    in
   32.14      roundup thy activate Morphism.identity (name, Morphism.identity) (marked, input')
   32.15 @@ -615,7 +615,7 @@
   32.16  fun add_declaration loc syntax decl =
   32.17    syntax ?
   32.18      Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
   32.19 -  #> add_thmss loc "" [(Attrib.empty_binding, Attrib.internal_declaration decl)];
   32.20 +  #> add_thmss loc "" [(Binding.empty_atts, Attrib.internal_declaration decl)];
   32.21  
   32.22  
   32.23  (*** Reasoning about locales ***)
    33.1 --- a/src/Pure/Isar/named_target.ML	Wed Jun 22 16:04:03 2016 +0200
    33.2 +++ b/src/Pure/Isar/named_target.ML	Thu Jun 23 11:01:14 2016 +0200
    33.3 @@ -109,7 +109,7 @@
    33.4          map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
    33.5            (#1 (Proof_Context.inferred_fixes ctxt));
    33.6        val assumes =
    33.7 -        map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
    33.8 +        map (fn A => (Binding.empty_atts, [(Thm.term_of A, [])]))
    33.9            (Assumption.all_assms_of ctxt);
   33.10        val elems =
   33.11          (if null fixes then [] else [Element.Fixes fixes]) @
    34.1 --- a/src/Pure/Isar/obtain.ML	Wed Jun 22 16:04:03 2016 +0200
    34.2 +++ b/src/Pure/Isar/obtain.ML	Thu Jun 23 11:01:14 2016 +0200
    34.3 @@ -228,7 +228,7 @@
    34.4      |> Proof.have true NONE after_qed
    34.5        [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
    34.6        [((that_binding, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
    34.7 -      [(Thm.empty_binding, [(thesis, [])])] int
    34.8 +      [(Binding.empty_atts, [(thesis, [])])] int
    34.9      |-> Proof.refine_insert
   34.10      |> Proof.map_context (fold Variable.bind_term binds')
   34.11    end;
   34.12 @@ -376,7 +376,7 @@
   34.13          |> Proof.fix (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
   34.14          |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm
   34.15            (obtain_export fix_ctxt rule (map (Thm.cterm_of ctxt) ts))
   34.16 -            [] [] [(Thm.empty_binding, asms)])
   34.17 +            [] [] [(Binding.empty_atts, asms)])
   34.18          |> Proof.map_context (fold Variable.unbind_term Auto_Bind.no_facts)
   34.19        end;
   34.20  
   34.21 @@ -403,7 +403,7 @@
   34.22      |> Proof.chain_facts chain_facts
   34.23      |> Proof.internal_goal print_result Proof_Context.mode_schematic true "guess"
   34.24        (SOME before_qed) after_qed
   34.25 -      [] [] [(Thm.empty_binding, [(Logic.mk_term goal, []), (goal, [])])]
   34.26 +      [] [] [(Binding.empty_atts, [(Logic.mk_term goal, []), (goal, [])])]
   34.27      |> snd
   34.28      |> Proof.refine_singleton
   34.29          (Method.primitive_text (fn _ => fn _ => Goal.init (Thm.cterm_of ctxt thesis)))
    35.1 --- a/src/Pure/Isar/parse_spec.ML	Wed Jun 22 16:04:03 2016 +0200
    35.2 +++ b/src/Pure/Isar/parse_spec.ML	Thu Jun 23 11:01:14 2016 +0200
    35.3 @@ -46,7 +46,7 @@
    35.4  fun opt_thm_name s =
    35.5    Scan.optional
    35.6      ((Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty) --| Parse.$$$ s)
    35.7 -    Attrib.empty_binding;
    35.8 +    Binding.empty_atts;
    35.9  
   35.10  val simple_spec = opt_thm_name ":" -- Parse.prop;
   35.11  val simple_specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop;
    36.1 --- a/src/Pure/Isar/proof.ML	Wed Jun 22 16:04:03 2016 +0200
    36.2 +++ b/src/Pure/Isar/proof.ML	Thu Jun 23 11:01:14 2016 +0200
    36.3 @@ -728,7 +728,7 @@
    36.4  
    36.5  (* note etc. *)
    36.6  
    36.7 -fun no_binding args = map (pair (Binding.empty, [])) args;
    36.8 +fun empty_bindings args = map (pair Binding.empty_atts) args;
    36.9  
   36.10  local
   36.11  
   36.12 @@ -746,13 +746,13 @@
   36.13  val note_thmss = gen_thmss (K []) I #2 (K I) (K I);
   36.14  val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute_cmd Proof_Context.get_fact;
   36.15  
   36.16 -val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
   36.17 +val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o empty_bindings;
   36.18  val from_thmss_cmd =
   36.19 -  gen_thmss (K []) chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding;
   36.20 +  gen_thmss (K []) chain #2 Attrib.attribute_cmd Proof_Context.get_fact o empty_bindings;
   36.21  
   36.22 -val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
   36.23 +val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o empty_bindings;
   36.24  val with_thmss_cmd =
   36.25 -  gen_thmss the_facts chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding;
   36.26 +  gen_thmss the_facts chain #2 Attrib.attribute_cmd Proof_Context.get_fact o empty_bindings;
   36.27  
   36.28  val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
   36.29  
   36.30 @@ -786,7 +786,7 @@
   36.31    |> assert_backward
   36.32    |> map_context_result
   36.33      (fn ctxt => ctxt |> Proof_Context.note_thmss ""
   36.34 -      (Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) (no_binding args)))
   36.35 +      (Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) (empty_bindings args)))
   36.36    |> (fn (named_facts, state') =>
   36.37      state' |> map_goal (fn (goal_ctxt, statement, using, goal, before_qed, after_qed) =>
   36.38        let
   36.39 @@ -855,7 +855,7 @@
   36.40  
   36.41      (*defs*)
   36.42      fun match_defs (((b, _, mx), (_, Free (x, T))) :: more_decls) ((((y, U), t), _) :: more_defs) =
   36.43 -          if x = y then ((b, mx), (Thm.empty_binding, t)) :: match_defs more_decls more_defs
   36.44 +          if x = y then ((b, mx), (Binding.empty_atts, t)) :: match_defs more_decls more_defs
   36.45            else
   36.46              error ("Mismatch of declaration " ^ show_term (Free (x, T)) ^ " wrt. definition " ^
   36.47                show_term (Free (y, U)))
    37.1 --- a/src/Pure/Isar/specification.ML	Wed Jun 22 16:04:03 2016 +0200
    37.2 +++ b/src/Pure/Isar/specification.ML	Thu Jun 23 11:01:14 2016 +0200
    37.3 @@ -378,7 +378,7 @@
    37.4              |> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.thatN, []), [(that, [])])]
    37.5              ||> Proof_Context.restore_stmt asms_ctxt;
    37.6  
    37.7 -          val stmt' = [((Binding.empty, []), [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])])];
    37.8 +          val stmt' = [(Binding.empty_atts, [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])])];
    37.9          in ((Obtain.obtains_attribs raw_obtains, prems, stmt', SOME that'), that_ctxt) end)
   37.10    end;
   37.11  
   37.12 @@ -399,12 +399,12 @@
   37.13          val results' =
   37.14            burrow (map (Goal.norm_result lthy) o Proof_Context.export goal_ctxt' lthy) results;
   37.15          val (res, lthy') =
   37.16 -          if forall (Attrib.is_empty_binding o fst) stmt then (map (pair "") results', lthy)
   37.17 +          if forall (Binding.is_empty_atts o fst) stmt then (map (pair "") results', lthy)
   37.18            else
   37.19              Local_Theory.notes_kind kind
   37.20                (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;
   37.21          val lthy'' =
   37.22 -          if Attrib.is_empty_binding (name, atts) then
   37.23 +          if Binding.is_empty_atts (name, atts) then
   37.24              (Proof_Display.print_results int pos lthy' ((kind, ""), res); lthy')
   37.25            else
   37.26              let
    38.1 --- a/src/Pure/Isar/subgoal.ML	Wed Jun 22 16:04:03 2016 +0200
    38.2 +++ b/src/Pure/Isar/subgoal.ML	Thu Jun 23 11:01:14 2016 +0200
    38.3 @@ -207,7 +207,7 @@
    38.4      val (prems_binding, do_prems) =
    38.5        (case raw_prems_binding of
    38.6          SOME (b, raw_atts) => ((b, map (prep_atts ctxt) raw_atts), true)
    38.7 -      | NONE => ((Binding.empty, []), false));
    38.8 +      | NONE => (Binding.empty_atts, false));
    38.9  
   38.10      val (subgoal_focus, _) =
   38.11        (if do_prems then focus else focus_params_fixed) ctxt
   38.12 @@ -239,7 +239,7 @@
   38.13        #context subgoal_focus
   38.14        |> Proof_Context.note_thmss "" [(prems_binding, [(#prems subgoal_focus, [])])] |> #2)
   38.15      |> Proof.internal_goal (K (K ())) (Proof_Context.get_mode ctxt) true "subgoal"
   38.16 -        NONE after_qed [] [] [(Thm.empty_binding, [(Thm.term_of (#concl subgoal_focus), [])])] |> #2
   38.17 +        NONE after_qed [] [] [(Binding.empty_atts, [(Thm.term_of (#concl subgoal_focus), [])])] |> #2
   38.18      |> Proof.using_facts facts
   38.19      |> pair subgoal_focus
   38.20    end;
    39.1 --- a/src/Pure/Pure.thy	Wed Jun 22 16:04:03 2016 +0200
    39.2 +++ b/src/Pure/Pure.thy	Thu Jun 23 11:01:14 2016 +0200
    39.3 @@ -408,14 +408,14 @@
    39.4    Parse_Spec.long_statement_keyword;
    39.5  
    39.6  val long_statement =
    39.7 -  Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Attrib.empty_binding --
    39.8 +  Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Binding.empty_atts --
    39.9    Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement
   39.10      >> (fn ((binding, includes), (elems, concl)) => (true, binding, includes, elems, concl));
   39.11  
   39.12  val short_statement =
   39.13    Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes
   39.14      >> (fn ((shows, assumes), fixes) =>
   39.15 -      (false, Attrib.empty_binding, [], [Element.Fixes fixes, Element.Assumes assumes],
   39.16 +      (false, Binding.empty_atts, [], [Element.Fixes fixes, Element.Assumes assumes],
   39.17          Element.Shows shows));
   39.18  
   39.19  fun theorem spec schematic descr =
   39.20 @@ -444,7 +444,7 @@
   39.21    Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems"
   39.22      (Parse.and_list1 Parse.thms1 -- Parse.for_fixes
   39.23        >> (fn (facts, fixes) =>
   39.24 -          #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
   39.25 +          #2 oo Specification.theorems_cmd "" [(Binding.empty_atts, flat facts)] fixes));
   39.26  
   39.27  val _ =
   39.28    Outer_Syntax.local_theory @{command_keyword named_theorems}
   39.29 @@ -915,7 +915,7 @@
   39.30  
   39.31  val opt_fact_binding =
   39.32    Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty)
   39.33 -    Attrib.empty_binding;
   39.34 +    Binding.empty_atts;
   39.35  
   39.36  val for_params =
   39.37    Scan.optional
    40.1 --- a/src/Pure/more_thm.ML	Wed Jun 22 16:04:03 2016 +0200
    40.2 +++ b/src/Pure/more_thm.ML	Thu Jun 23 11:01:14 2016 +0200
    40.3 @@ -83,7 +83,6 @@
    40.4    val add_def_global: bool -> bool -> binding * term -> theory -> (string * thm) * theory
    40.5    type attribute = Context.generic * thm -> Context.generic option * thm option
    40.6    type binding = binding * attribute list
    40.7 -  val empty_binding: binding
    40.8    val tag_rule: string * string -> thm -> thm
    40.9    val untag_rule: string -> thm -> thm
   40.10    val is_free_dummy: thm -> bool
   40.11 @@ -597,7 +596,6 @@
   40.12  type attribute = Context.generic * thm -> Context.generic option * thm option;
   40.13  
   40.14  type binding = binding * attribute list;
   40.15 -val empty_binding: binding = (Binding.empty, []);
   40.16  
   40.17  fun rule_attribute ths f (x, th) =
   40.18    (NONE,