binding replaces bstring
authorhaftmann
Wed Jan 21 18:27:43 2009 +0100 (2009-01-21)
changeset 29585c23295521af5
parent 29584 88ba5e5ac6d8
child 29586 4f9803829625
binding replaces bstring
src/HOL/Import/hol4rews.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/replay.ML
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Nominal/nominal_thmdecls.ML
src/HOLCF/Tools/domain/domain_axioms.ML
src/HOLCF/Tools/domain/domain_extender.ML
src/HOLCF/Tools/domain/domain_theorems.ML
src/HOLCF/Tools/fixrec_package.ML
src/HOLCF/Tools/pcpodef_package.ML
     1.1 --- a/src/HOL/Import/hol4rews.ML	Wed Jan 21 16:51:45 2009 +0100
     1.2 +++ b/src/HOL/Import/hol4rews.ML	Wed Jan 21 18:27:43 2009 +0100
     1.3 @@ -390,7 +390,7 @@
     1.4          val thm2 = standard thm1;
     1.5        in
     1.6          thy
     1.7 -        |> PureThy.store_thm (bthm, thm2)
     1.8 +        |> PureThy.store_thm (Binding.name bthm, thm2)
     1.9          |> snd
    1.10          |> add_hol4_theorem bthy bthm hth
    1.11        end;
     2.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Jan 21 16:51:45 2009 +0100
     2.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Jan 21 18:27:43 2009 +0100
     2.3 @@ -1928,7 +1928,7 @@
     2.4                         Replaying _ => thy
     2.5                       | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; Sign.add_consts_i [(constname,ctype,csyn)] thy)
     2.6          val eq = mk_defeq constname rhs' thy1
     2.7 -        val (thms, thy2) = PureThy.add_defs false [((thmname,eq),[])] thy1
     2.8 +        val (thms, thy2) = PureThy.add_defs false [((Binding.name thmname,eq),[])] thy1
     2.9          val _ = ImportRecorder.add_defs thmname eq
    2.10          val def_thm = hd thms
    2.11          val thm' = def_thm RS meta_eq_to_obj_eq_thm
     3.1 --- a/src/HOL/Import/replay.ML	Wed Jan 21 16:51:45 2009 +0100
     3.2 +++ b/src/HOL/Import/replay.ML	Wed Jan 21 18:27:43 2009 +0100
     3.3 @@ -340,7 +340,7 @@
     3.4  	  | delta (Hol_move (fullname, moved_thmname)) thy = 
     3.5  	    add_hol4_move fullname moved_thmname thy
     3.6  	  | delta (Defs (thmname, eq)) thy =
     3.7 -	    snd (PureThy.add_defs false [((thmname, eq), [])] thy)
     3.8 +	    snd (PureThy.add_defs false [((Binding.name thmname, eq), [])] thy)
     3.9  	  | delta (Hol_theorem (thyname, thmname, th)) thy =
    3.10  	    add_hol4_theorem thyname thmname ([], th_of thy th) thy
    3.11  	  | delta (Typedef (thmname, typ, c, repabs, th)) thy = 
     4.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Jan 21 16:51:45 2009 +0100
     4.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Jan 21 18:27:43 2009 +0100
     4.3 @@ -90,6 +90,9 @@
     4.4    let val T = fastype_of x
     4.5    in Const ("List.list.Cons", T --> HOLogic.listT T --> HOLogic.listT T) $ x $ xs end;
     4.6  
     4.7 +fun add_thms_string args = PureThy.add_thms ((map o apfst o apfst) Binding.name args);
     4.8 +fun add_thmss_string args = PureThy.add_thmss ((map o apfst o apfst) Binding.name args);
     4.9 +
    4.10  (* this function sets up all matters related to atom-  *)
    4.11  (* kinds; the user specifies a list of atom-kind names *)
    4.12  (* atom_decl <ak1> ... <akn>                           *)
    4.13 @@ -121,7 +124,7 @@
    4.14                                            atac 1]
    4.15               
    4.16                val (inj_thm,thy2) = 
    4.17 -                   PureThy.add_thms [((ak^"_inj",Goal.prove_global thy1 [] [] stmnt1 proof1), [])] thy1
    4.18 +                   add_thms_string [((ak^"_inj",Goal.prove_global thy1 [] [] stmnt1 proof1), [])] thy1
    4.19                
    4.20                (* second statement *)
    4.21                val y = Free ("y",ak_type)  
    4.22 @@ -136,7 +139,7 @@
    4.23  
    4.24                (* third statement *)
    4.25                val (inject_thm,thy3) =
    4.26 -                  PureThy.add_thms [((ak^"_injection",Goal.prove_global thy2 [] [] stmnt2 proof2), [])] thy2
    4.27 +                  add_thms_string [((ak^"_injection",Goal.prove_global thy2 [] [] stmnt2 proof2), [])] thy2
    4.28    
    4.29                val stmnt3 = HOLogic.mk_Trueprop
    4.30                             (HOLogic.mk_not
    4.31 @@ -152,7 +155,7 @@
    4.32                                            simp_tac (HOL_basic_ss addsimps simp3) 1]  
    4.33             
    4.34                val (inf_thm,thy4) =  
    4.35 -                    PureThy.add_thms [((ak^"_infinite",Goal.prove_global thy3 [] [] stmnt3 proof3), [])] thy3
    4.36 +                    add_thms_string [((ak^"_infinite",Goal.prove_global thy3 [] [] stmnt3 proof3), [])] thy3
    4.37            in 
    4.38              ((inj_thm,inject_thm,inf_thm),thy4)
    4.39            end) ak_names thy
    4.40 @@ -186,7 +189,7 @@
    4.41          val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
    4.42        in
    4.43          thy |> Sign.add_consts_i [("swap_" ^ ak_name, swapT, NoSyn)] 
    4.44 -            |> PureThy.add_defs_unchecked true [((name, def2),[])]
    4.45 +            |> PureThy.add_defs_unchecked true [((Binding.name name, def2),[])]
    4.46              |> snd
    4.47              |> OldPrimrecPackage.add_primrec_unchecked_i "" [(("", def1),[])]
    4.48        end) ak_names_types thy1;
    4.49 @@ -241,14 +244,14 @@
    4.50            val def = Logic.mk_equals
    4.51                      (cperm $ pi $ a, if ak_name = ak_name' then cperm_def $ pi $ a else a)
    4.52          in
    4.53 -          PureThy.add_defs_unchecked true [((name, def),[])] thy'
    4.54 +          PureThy.add_defs_unchecked true [((Binding.name name, def),[])] thy'
    4.55          end) ak_names_types thy) ak_names_types thy4;
    4.56      
    4.57      (* proves that every atom-kind is an instance of at *)
    4.58      (* lemma at_<ak>_inst:                              *)
    4.59      (* at TYPE(<ak>)                                    *)
    4.60      val (prm_cons_thms,thy6) = 
    4.61 -      thy5 |> PureThy.add_thms (map (fn (ak_name, T) =>
    4.62 +      thy5 |> add_thms_string (map (fn (ak_name, T) =>
    4.63        let
    4.64          val ak_name_qu = Sign.full_bname thy5 (ak_name);
    4.65          val i_type = Type(ak_name_qu,[]);
    4.66 @@ -309,7 +312,7 @@
    4.67      (* lemma pt_<ak>_inst:                                    *)
    4.68      (* pt TYPE('x::pt_<ak>) TYPE(<ak>)                        *)
    4.69      val (prm_inst_thms,thy8) = 
    4.70 -      thy7 |> PureThy.add_thms (map (fn (ak_name, T) =>
    4.71 +      thy7 |> add_thms_string (map (fn (ak_name, T) =>
    4.72        let
    4.73          val ak_name_qu = Sign.full_bname thy7 ak_name;
    4.74          val pt_name_qu = Sign.full_bname thy7 ("pt_"^ak_name);
    4.75 @@ -355,7 +358,7 @@
    4.76       (* lemma abst_<ak>_inst:                                    *)
    4.77       (* fs TYPE('x::pt_<ak>) TYPE (<ak>)                         *)
    4.78       val (fs_inst_thms,thy12) = 
    4.79 -       thy11 |> PureThy.add_thms (map (fn (ak_name, T) =>
    4.80 +       thy11 |> add_thms_string (map (fn (ak_name, T) =>
    4.81         let
    4.82           val ak_name_qu = Sign.full_bname thy11 ak_name;
    4.83           val fs_name_qu = Sign.full_bname thy11 ("fs_"^ak_name);
    4.84 @@ -428,7 +431,7 @@
    4.85                                          rtac allI 1, rtac allI 1, rtac allI 1,
    4.86                                          rtac cp1 1];
    4.87             in
    4.88 -             yield_singleton PureThy.add_thms ((name,
    4.89 +             yield_singleton add_thms_string ((name,
    4.90                 Goal.prove_global thy' [] [] statement proof), []) thy'
    4.91             end) 
    4.92             ak_names_types thy) ak_names_types thy12b;
    4.93 @@ -460,7 +463,7 @@
    4.94  
    4.95                   val proof = fn _ => simp_tac simp_s 1;
    4.96                 in
    4.97 -                PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy'
    4.98 +                add_thms_string [((name, Goal.prove_global thy' [] [] statement proof), [])] thy'
    4.99                 end
   4.100             else 
   4.101              ([],thy')))  (* do nothing branch, if ak_name = ak_name' *) 
   4.102 @@ -870,114 +873,114 @@
   4.103               fun inst_pt_pt_at_cp_dj thms = inst_zip djs (inst_pt_pt_at_cp thms);
   4.104             in
   4.105              thy32 
   4.106 -            |>   PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])]
   4.107 -            ||>> PureThy.add_thmss [(("alpha'", inst_pt_at [abs_fun_eq']),[])]
   4.108 -            ||>> PureThy.add_thmss [(("alpha_fresh", inst_pt_at [abs_fun_fresh]),[])]
   4.109 -            ||>> PureThy.add_thmss [(("alpha_fresh'", inst_pt_at [abs_fun_fresh']),[])]
   4.110 -            ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij] @ inst_pt_at [pt_swap_bij']),[])]
   4.111 -            ||>> PureThy.add_thmss 
   4.112 +            |>   add_thmss_string [(("alpha", inst_pt_at [abs_fun_eq]),[])]
   4.113 +            ||>> add_thmss_string [(("alpha'", inst_pt_at [abs_fun_eq']),[])]
   4.114 +            ||>> add_thmss_string [(("alpha_fresh", inst_pt_at [abs_fun_fresh]),[])]
   4.115 +            ||>> add_thmss_string [(("alpha_fresh'", inst_pt_at [abs_fun_fresh']),[])]
   4.116 +            ||>> add_thmss_string [(("perm_swap", inst_pt_at [pt_swap_bij] @ inst_pt_at [pt_swap_bij']),[])]
   4.117 +            ||>> add_thmss_string 
   4.118  	      let val thms1 = inst_at at_swap_simps
   4.119                    and thms2 = inst_dj [dj_perm_forget]
   4.120                in [(("swap_simps", thms1 @ thms2),[])] end 
   4.121 -            ||>> PureThy.add_thmss 
   4.122 +            ||>> add_thmss_string 
   4.123                let val thms1 = inst_pt_at [pt_pi_rev];
   4.124                    val thms2 = inst_pt_at [pt_rev_pi];
   4.125                in [(("perm_pi_simp",thms1 @ thms2),[])] end
   4.126 -            ||>> PureThy.add_thmss [(("perm_fresh_fresh", inst_pt_at [pt_fresh_fresh]),[])]
   4.127 -            ||>> PureThy.add_thmss [(("perm_bij", inst_pt_at [pt_bij]),[])]
   4.128 -            ||>> PureThy.add_thmss 
   4.129 +            ||>> add_thmss_string [(("perm_fresh_fresh", inst_pt_at [pt_fresh_fresh]),[])]
   4.130 +            ||>> add_thmss_string [(("perm_bij", inst_pt_at [pt_bij]),[])]
   4.131 +            ||>> add_thmss_string 
   4.132                let val thms1 = inst_pt_at [pt_perm_compose];
   4.133                    val thms2 = instR cp1 (Library.flat cps');
   4.134                in [(("perm_compose",thms1 @ thms2),[])] end
   4.135 -            ||>> PureThy.add_thmss [(("perm_compose'",inst_pt_at [pt_perm_compose']),[])] 
   4.136 -            ||>> PureThy.add_thmss [(("perm_app", inst_pt_at [perm_app]),[])]
   4.137 -            ||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
   4.138 -            ||>> PureThy.add_thmss [(("exists_fresh", inst_at [at_exists_fresh]),[])]
   4.139 -            ||>> PureThy.add_thmss [(("exists_fresh'", inst_at [at_exists_fresh']),[])]
   4.140 -            ||>> PureThy.add_thmss
   4.141 +            ||>> add_thmss_string [(("perm_compose'",inst_pt_at [pt_perm_compose']),[])] 
   4.142 +            ||>> add_thmss_string [(("perm_app", inst_pt_at [perm_app]),[])]
   4.143 +            ||>> add_thmss_string [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
   4.144 +            ||>> add_thmss_string [(("exists_fresh", inst_at [at_exists_fresh]),[])]
   4.145 +            ||>> add_thmss_string [(("exists_fresh'", inst_at [at_exists_fresh']),[])]
   4.146 +            ||>> add_thmss_string
   4.147                let
   4.148                  val thms1 = inst_pt_at [all_eqvt];
   4.149                  val thms2 = map (fold_rule [inductive_forall_def]) thms1
   4.150                in
   4.151                  [(("all_eqvt", thms1 @ thms2), [NominalThmDecls.eqvt_force_add])]
   4.152                end
   4.153 -            ||>> PureThy.add_thmss [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_force_add])]
   4.154 -            ||>> PureThy.add_thmss [(("ex1_eqvt", inst_pt_at [ex1_eqvt]),[NominalThmDecls.eqvt_force_add])]
   4.155 -            ||>> PureThy.add_thmss [(("the_eqvt", inst_pt_at [the_eqvt]),[NominalThmDecls.eqvt_force_add])]
   4.156 -            ||>> PureThy.add_thmss 
   4.157 +            ||>> add_thmss_string [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_force_add])]
   4.158 +            ||>> add_thmss_string [(("ex1_eqvt", inst_pt_at [ex1_eqvt]),[NominalThmDecls.eqvt_force_add])]
   4.159 +            ||>> add_thmss_string [(("the_eqvt", inst_pt_at [the_eqvt]),[NominalThmDecls.eqvt_force_add])]
   4.160 +            ||>> add_thmss_string 
   4.161                let val thms1 = inst_at [at_fresh]
   4.162                    val thms2 = inst_dj [at_fresh_ineq]
   4.163                in [(("fresh_atm", thms1 @ thms2),[])] end
   4.164 -            ||>> PureThy.add_thmss
   4.165 +            ||>> add_thmss_string
   4.166                let val thms1 = inst_at at_calc
   4.167                    and thms2 = inst_dj [dj_perm_forget]
   4.168                in [(("calc_atm", thms1 @ thms2),[])] end
   4.169 -            ||>> PureThy.add_thmss
   4.170 +            ||>> add_thmss_string
   4.171                let val thms1 = inst_pt_at [abs_fun_pi]
   4.172                    and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq]
   4.173                in [(("abs_perm", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end
   4.174 -            ||>> PureThy.add_thmss
   4.175 +            ||>> add_thmss_string
   4.176                let val thms1 = inst_dj [dj_perm_forget]
   4.177                    and thms2 = inst_dj [dj_pp_forget]
   4.178                in [(("perm_dj", thms1 @ thms2),[])] end
   4.179 -            ||>> PureThy.add_thmss
   4.180 +            ||>> add_thmss_string
   4.181                let val thms1 = inst_pt_at_fs [fresh_iff]
   4.182                    and thms2 = inst_pt_at [fresh_iff]
   4.183                    and thms3 = inst_pt_pt_at_cp_dj [fresh_iff_ineq]
   4.184              in [(("abs_fresh", thms1 @ thms2 @ thms3),[])] end
   4.185 -            ||>> PureThy.add_thmss
   4.186 +            ||>> add_thmss_string
   4.187                let val thms1 = inst_pt_at [abs_fun_supp]
   4.188                    and thms2 = inst_pt_at_fs [abs_fun_supp]
   4.189                    and thms3 = inst_pt_pt_at_cp_dj [abs_fun_supp_ineq]
   4.190                in [(("abs_supp", thms1 @ thms2 @ thms3),[])] end
   4.191 -            ||>> PureThy.add_thmss
   4.192 +            ||>> add_thmss_string
   4.193                let val thms1 = inst_pt_at [fresh_left]
   4.194                    and thms2 = inst_pt_pt_at_cp [fresh_left_ineq]
   4.195                in [(("fresh_left", thms1 @ thms2),[])] end
   4.196 -            ||>> PureThy.add_thmss
   4.197 +            ||>> add_thmss_string
   4.198                let val thms1 = inst_pt_at [fresh_right]
   4.199                    and thms2 = inst_pt_pt_at_cp [fresh_right_ineq]
   4.200                in [(("fresh_right", thms1 @ thms2),[])] end
   4.201 -            ||>> PureThy.add_thmss
   4.202 +            ||>> add_thmss_string
   4.203                let val thms1 = inst_pt_at [fresh_bij]
   4.204                    and thms2 = inst_pt_pt_at_cp [fresh_bij_ineq]
   4.205                in [(("fresh_bij", thms1 @ thms2),[])] end
   4.206 -            ||>> PureThy.add_thmss
   4.207 +            ||>> add_thmss_string
   4.208                let val thms1 = inst_pt_at fresh_star_bij
   4.209                    and thms2 = flat (map (fn ti => inst_pt_pt_at_cp [ti]) fresh_star_bij_ineq);
   4.210                in [(("fresh_star_bij", thms1 @ thms2),[])] end
   4.211 -            ||>> PureThy.add_thmss
   4.212 +            ||>> add_thmss_string
   4.213                let val thms1 = inst_pt_at [fresh_eqvt]
   4.214                    and thms2 = inst_pt_pt_at_cp_dj [fresh_eqvt_ineq]
   4.215                in [(("fresh_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end
   4.216 -            ||>> PureThy.add_thmss
   4.217 +            ||>> add_thmss_string
   4.218                let val thms1 = inst_pt_at [in_eqvt]
   4.219                in [(("in_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
   4.220 -            ||>> PureThy.add_thmss
   4.221 +            ||>> add_thmss_string
   4.222                let val thms1 = inst_pt_at [eq_eqvt]
   4.223                in [(("eq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
   4.224 -            ||>> PureThy.add_thmss
   4.225 +            ||>> add_thmss_string
   4.226                let val thms1 = inst_pt_at [set_diff_eqvt]
   4.227                in [(("set_diff_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
   4.228 -            ||>> PureThy.add_thmss
   4.229 +            ||>> add_thmss_string
   4.230                let val thms1 = inst_pt_at [subseteq_eqvt]
   4.231                in [(("subseteq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
   4.232 -            ||>> PureThy.add_thmss [(("insert_eqvt", inst_pt_at [insert_eqvt]), [NominalThmDecls.eqvt_add])]
   4.233 -            ||>> PureThy.add_thmss [(("set_eqvt", inst_pt_at [set_eqvt]), [NominalThmDecls.eqvt_add])]
   4.234 -            ||>> PureThy.add_thmss [(("perm_set_eq", inst_pt_at [perm_set_eq]), [])]
   4.235 -            ||>> PureThy.add_thmss
   4.236 +            ||>> add_thmss_string [(("insert_eqvt", inst_pt_at [insert_eqvt]), [NominalThmDecls.eqvt_add])]
   4.237 +            ||>> add_thmss_string [(("set_eqvt", inst_pt_at [set_eqvt]), [NominalThmDecls.eqvt_add])]
   4.238 +            ||>> add_thmss_string [(("perm_set_eq", inst_pt_at [perm_set_eq]), [])]
   4.239 +            ||>> add_thmss_string
   4.240                let val thms1 = inst_pt_at [fresh_aux]
   4.241                    and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] 
   4.242                in  [(("fresh_aux", thms1 @ thms2),[])] end  
   4.243 -            ||>> PureThy.add_thmss
   4.244 +            ||>> add_thmss_string
   4.245                let val thms1 = inst_pt_at [fresh_perm_app]
   4.246                    and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] 
   4.247                in  [(("fresh_perm_app", thms1 @ thms2),[])] end 
   4.248 -            ||>> PureThy.add_thmss
   4.249 +            ||>> add_thmss_string
   4.250                let val thms1 = inst_pt_at [pt_perm_supp]
   4.251                    and thms2 = inst_pt_pt_at_cp [pt_perm_supp_ineq] 
   4.252                in  [(("supp_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end  
   4.253 -            ||>> PureThy.add_thmss [(("fin_supp",fs_axs),[])]
   4.254 +            ||>> add_thmss_string [(("fin_supp",fs_axs),[])]
   4.255             end;
   4.256  
   4.257      in 
     5.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed Jan 21 16:51:45 2009 +0100
     5.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Jan 21 18:27:43 2009 +0100
     5.3 @@ -562,17 +562,17 @@
     5.4              [ind_case_names, RuleCases.consumes 1]);
     5.5          val ([strong_induct'], thy') = thy |>
     5.6            Sign.add_path rec_name |>
     5.7 -          PureThy.add_thms [(("strong_induct", #1 strong_induct), #2 strong_induct)];
     5.8 +          PureThy.add_thms [((Binding.name "strong_induct", #1 strong_induct), #2 strong_induct)];
     5.9          val strong_inducts =
    5.10            ProjectRule.projects ctxt (1 upto length names) strong_induct'
    5.11        in
    5.12          thy' |>
    5.13 -        PureThy.add_thmss [(("strong_inducts", strong_inducts),
    5.14 +        PureThy.add_thmss [((Binding.name "strong_inducts", strong_inducts),
    5.15            [ind_case_names, RuleCases.consumes 1])] |> snd |>
    5.16          Sign.parent_path |>
    5.17          fold (fn ((name, elim), (_, cases)) =>
    5.18            Sign.add_path (Sign.base_name name) #>
    5.19 -          PureThy.add_thms [(("strong_cases", elim),
    5.20 +          PureThy.add_thms [((Binding.name "strong_cases", elim),
    5.21              [RuleCases.case_names (map snd cases),
    5.22               RuleCases.consumes 1])] #> snd #>
    5.23            Sign.parent_path) (strong_cases ~~ induct_cases')
    5.24 @@ -653,7 +653,7 @@
    5.25    in
    5.26      fold (fn (name, ths) =>
    5.27        Sign.add_path (Sign.base_name name) #>
    5.28 -      PureThy.add_thmss [(("eqvt", ths), [NominalThmDecls.eqvt_add])] #> snd #>
    5.29 +      PureThy.add_thmss [((Binding.name "eqvt", ths), [NominalThmDecls.eqvt_add])] #> snd #>
    5.30        Sign.parent_path) (names ~~ transp thss) thy
    5.31    end;
    5.32  
     6.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Jan 21 16:51:45 2009 +0100
     6.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Jan 21 18:27:43 2009 +0100
     6.3 @@ -458,12 +458,12 @@
     6.4              [ind_case_names, RuleCases.consumes 1]);
     6.5          val ([strong_induct'], thy') = thy |>
     6.6            Sign.add_path rec_name |>
     6.7 -          PureThy.add_thms [(("strong_induct", #1 strong_induct), #2 strong_induct)];
     6.8 +          PureThy.add_thms [((Binding.name "strong_induct", #1 strong_induct), #2 strong_induct)];
     6.9          val strong_inducts =
    6.10            ProjectRule.projects ctxt (1 upto length names) strong_induct'
    6.11        in
    6.12          thy' |>
    6.13 -        PureThy.add_thmss [(("strong_inducts", strong_inducts),
    6.14 +        PureThy.add_thmss [((Binding.name "strong_inducts", strong_inducts),
    6.15            [ind_case_names, RuleCases.consumes 1])] |> snd |>
    6.16          Sign.parent_path
    6.17        end))
     7.1 --- a/src/HOL/Nominal/nominal_package.ML	Wed Jan 21 16:51:45 2009 +0100
     7.2 +++ b/src/HOL/Nominal/nominal_package.ML	Wed Jan 21 18:27:43 2009 +0100
     7.3 @@ -490,13 +490,13 @@
     7.4              (full_new_type_names' ~~ tyvars) thy
     7.5          end) atoms |>
     7.6        PureThy.add_thmss
     7.7 -        [((space_implode "_" new_type_names ^ "_unfolded_perm_eq",
     7.8 +        [((Binding.name (space_implode "_" new_type_names ^ "_unfolded_perm_eq"),
     7.9            unfolded_perm_eq_thms), [Simplifier.simp_add]),
    7.10 -         ((space_implode "_" new_type_names ^ "_perm_empty",
    7.11 +         ((Binding.name (space_implode "_" new_type_names ^ "_perm_empty"),
    7.12            perm_empty_thms), [Simplifier.simp_add]),
    7.13 -         ((space_implode "_" new_type_names ^ "_perm_append",
    7.14 +         ((Binding.name (space_implode "_" new_type_names ^ "_perm_append"),
    7.15            perm_append_thms), [Simplifier.simp_add]),
    7.16 -         ((space_implode "_" new_type_names ^ "_perm_eq",
    7.17 +         ((Binding.name (space_implode "_" new_type_names ^ "_perm_eq"),
    7.18            perm_eq_thms), [Simplifier.simp_add])];
    7.19  
    7.20      (**** Define representing sets ****)
    7.21 @@ -627,7 +627,7 @@
    7.22            val pi = Free ("pi", permT);
    7.23            val T = Type (Sign.intern_type thy name, map TFree tvs);
    7.24          in apfst (pair r o hd)
    7.25 -          (PureThy.add_defs_unchecked true [(("prm_" ^ name ^ "_def", Logic.mk_equals
    7.26 +          (PureThy.add_defs_unchecked true [((Binding.name ("prm_" ^ name ^ "_def"), Logic.mk_equals
    7.27              (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
    7.28               Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $
    7.29                 (Const ("Nominal.perm", permT --> U --> U) $ pi $
    7.30 @@ -801,7 +801,7 @@
    7.31          val def_name = (Sign.base_name cname) ^ "_def";
    7.32          val ([def_thm], thy') = thy |>
    7.33            Sign.add_consts_i [(cname', constrT, mx)] |>
    7.34 -          (PureThy.add_defs false o map Thm.no_attributes) [(def_name, def)]
    7.35 +          (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]
    7.36        in (thy', defs @ [def_thm], eqns @ [eqn]) end;
    7.37  
    7.38      fun dt_constr_defs ((thy, defs, eqns, dist_lemmas), ((((((_, (_, _, constrs)),
    7.39 @@ -1114,8 +1114,8 @@
    7.40   
    7.41      val (_, thy9) = thy8 |>
    7.42        Sign.add_path big_name |>
    7.43 -      PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] ||>>
    7.44 -      PureThy.add_thmss [(("inducts", projections dt_induct), [case_names_induct])] ||>
    7.45 +      PureThy.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])] ||>>
    7.46 +      PureThy.add_thmss [((Binding.name "inducts", projections dt_induct), [case_names_induct])] ||>
    7.47        Sign.parent_path ||>>
    7.48        DatatypeAux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>>
    7.49        DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>>
    7.50 @@ -1405,9 +1405,9 @@
    7.51  
    7.52      val (_, thy10) = thy9 |>
    7.53        Sign.add_path big_name |>
    7.54 -      PureThy.add_thms [(("strong_induct'", induct_aux), [])] ||>>
    7.55 -      PureThy.add_thms [(("strong_induct", induct), [case_names_induct])] ||>>
    7.56 -      PureThy.add_thmss [(("strong_inducts", projections induct), [case_names_induct])];
    7.57 +      PureThy.add_thms [((Binding.name "strong_induct'", induct_aux), [])] ||>>
    7.58 +      PureThy.add_thms [((Binding.name "strong_induct", induct), [case_names_induct])] ||>>
    7.59 +      PureThy.add_thmss [((Binding.name "strong_inducts", projections induct), [case_names_induct])];
    7.60  
    7.61      (**** recursion combinator ****)
    7.62  
    7.63 @@ -2015,7 +2015,7 @@
    7.64            (Sign.base_name name, rec_fn_Ts @ [T] ---> T', NoSyn))
    7.65            (reccomb_names ~~ recTs ~~ rec_result_Ts))
    7.66        |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
    7.67 -          ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T,
    7.68 +          (Binding.name (Sign.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
    7.69             Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
    7.70               set $ Free ("x", T) $ Free ("y", T'))))))
    7.71                 (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
    7.72 @@ -2052,12 +2052,12 @@
    7.73      (* FIXME: theorems are stored in database for testing only *)
    7.74      val (_, thy13) = thy12 |>
    7.75        PureThy.add_thmss
    7.76 -        [(("rec_equiv", List.concat rec_equiv_thms), []),
    7.77 -         (("rec_equiv'", List.concat rec_equiv_thms'), []),
    7.78 -         (("rec_fin_supp", List.concat rec_fin_supp_thms), []),
    7.79 -         (("rec_fresh", List.concat rec_fresh_thms), []),
    7.80 -         (("rec_unique", map standard rec_unique_thms), []),
    7.81 -         (("recs", rec_thms), [])] ||>
    7.82 +        [((Binding.name "rec_equiv", List.concat rec_equiv_thms), []),
    7.83 +         ((Binding.name "rec_equiv'", List.concat rec_equiv_thms'), []),
    7.84 +         ((Binding.name "rec_fin_supp", List.concat rec_fin_supp_thms), []),
    7.85 +         ((Binding.name "rec_fresh", List.concat rec_fresh_thms), []),
    7.86 +         ((Binding.name "rec_unique", map standard rec_unique_thms), []),
    7.87 +         ((Binding.name "recs", rec_thms), [])] ||>
    7.88        Sign.parent_path ||>
    7.89        map_nominal_datatypes (fold Symtab.update dt_infos);
    7.90  
     8.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Wed Jan 21 16:51:45 2009 +0100
     8.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Wed Jan 21 18:27:43 2009 +0100
     8.3 @@ -187,8 +187,8 @@
     8.4          "equivariance theorem declaration (without checking the form of the lemma)"),
     8.5        ("fresh", Attrib.add_del_args fresh_add fresh_del, "freshness theorem declaration"),
     8.6        ("bij",   Attrib.add_del_args bij_add bij_del,     "bijection theorem declaration")] #>
     8.7 -  PureThy.add_thms_dynamic ("eqvts", #eqvts o Data.get) #>
     8.8 -  PureThy.add_thms_dynamic ("freshs", #freshs o Data.get) #>
     8.9 -  PureThy.add_thms_dynamic ("bijs", #bijs o Data.get);
    8.10 +  PureThy.add_thms_dynamic (Binding.name "eqvts", #eqvts o Data.get) #>
    8.11 +  PureThy.add_thms_dynamic (Binding.name "freshs", #freshs o Data.get) #>
    8.12 +  PureThy.add_thms_dynamic (Binding.name "bijs", #bijs o Data.get);
    8.13  
    8.14  end;
     9.1 --- a/src/HOLCF/Tools/domain/domain_axioms.ML	Wed Jan 21 16:51:45 2009 +0100
     9.2 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML	Wed Jan 21 18:27:43 2009 +0100
     9.3 @@ -111,10 +111,10 @@
     9.4  
     9.5  fun infer_props thy = map (apsnd (FixrecPackage.legacy_infer_prop thy));
     9.6  
     9.7 -fun add_axioms_i x = snd o PureThy.add_axioms (map Thm.no_attributes x);
     9.8 +fun add_axioms_i x = snd o PureThy.add_axioms (map (Thm.no_attributes o apfst Binding.name) x);
     9.9  fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy;
    9.10  
    9.11 -fun add_defs_i x = snd o (PureThy.add_defs false) (map Thm.no_attributes x);
    9.12 +fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x);
    9.13  fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
    9.14  
    9.15  in (* local *)
    10.1 --- a/src/HOLCF/Tools/domain/domain_extender.ML	Wed Jan 21 16:51:45 2009 +0100
    10.2 +++ b/src/HOLCF/Tools/domain/domain_extender.ML	Wed Jan 21 18:27:43 2009 +0100
    10.3 @@ -134,7 +134,7 @@
    10.4    in
    10.5      theorems_thy
    10.6      |> Sign.add_path (Sign.base_name comp_dnam)
    10.7 -    |> (snd o (PureThy.add_thmss [(("rews", List.concat rewss @ take_rews), [])]))
    10.8 +    |> (snd o (PureThy.add_thmss [((Binding.name "rews", List.concat rewss @ take_rews), [])]))
    10.9      |> Sign.parent_path
   10.10    end;
   10.11  
    11.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Jan 21 16:51:45 2009 +0100
    11.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Jan 21 18:27:43 2009 +0100
    11.3 @@ -607,7 +607,7 @@
    11.4  in
    11.5    thy
    11.6      |> Sign.add_path (Sign.base_name dname)
    11.7 -    |> (snd o (PureThy.add_thmss (map Thm.no_attributes [
    11.8 +    |> (snd o (PureThy.add_thmss (map (Thm.no_attributes o apfst Binding.name) [
    11.9          ("iso_rews" , iso_rews  ),
   11.10          ("exhaust"  , [exhaust] ),
   11.11          ("casedist" , [casedist]),
   11.12 @@ -623,7 +623,7 @@
   11.13          ("injects" , injects ),
   11.14          ("copy_rews", copy_rews)])))
   11.15      |> (snd o PureThy.add_thmss
   11.16 -        [(("match_rews", mat_rews), [Simplifier.simp_add])])
   11.17 +        [((Binding.name "match_rews", mat_rews), [Simplifier.simp_add])])
   11.18      |> Sign.parent_path
   11.19      |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
   11.20          pat_rews @ dist_les @ dist_eqs @ copy_rews)
   11.21 @@ -1000,7 +1000,7 @@
   11.22  end; (* local *)
   11.23  
   11.24  in thy |> Sign.add_path comp_dnam
   11.25 -       |> (snd o (PureThy.add_thmss (map Thm.no_attributes [
   11.26 +       |> (snd o (PureThy.add_thmss (map (Thm.no_attributes o apfst Binding.name) [
   11.27  		("take_rews"  , take_rews  ),
   11.28  		("take_lemmas", take_lemmas),
   11.29  		("finites"    , finites    ),
    12.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Wed Jan 21 16:51:45 2009 +0100
    12.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Wed Jan 21 18:27:43 2009 +0100
    12.3 @@ -96,7 +96,7 @@
    12.4      
    12.5      val fixdefs = map (apsnd (legacy_infer_prop thy)) pre_fixdefs;
    12.6      val (fixdef_thms, thy') =
    12.7 -      PureThy.add_defs false (map Thm.no_attributes fixdefs) thy;
    12.8 +      PureThy.add_defs false (map (Thm.no_attributes o apfst Binding.name) fixdefs) thy;
    12.9      val ctuple_fixdef_thm = foldr1 (fn (x,y) => @{thm cpair_equalI} OF [x,y]) fixdef_thms;
   12.10      
   12.11      val ctuple_unfold = legacy_infer_term thy' (mk_trp (mk_ctuple lhss === mk_ctuple rhss));
   12.12 @@ -114,7 +114,7 @@
   12.13          in (n^"_unfold", thmL) :: unfolds ns thmR end;
   12.14      val unfold_thms = unfolds names ctuple_unfold_thm;
   12.15      val thms = ctuple_induct_thm :: unfold_thms;
   12.16 -    val (_, thy'') = PureThy.add_thms (map Thm.no_attributes thms) thy';
   12.17 +    val (_, thy'') = PureThy.add_thms (map (Thm.no_attributes o apfst Binding.name) thms) thy';
   12.18    in
   12.19      (thy'', names, fixdef_thms, map snd unfold_thms)
   12.20    end;
   12.21 @@ -241,14 +241,14 @@
   12.22    in
   12.23      if strict then let (* only prove simp rules if strict = true *)
   12.24        val eqn_blocks = unconcat lengths ((names ~~ eqn_ts') ~~ atts);
   12.25 -      val simps = List.concat (map (make_simps thy') (unfold_thms ~~ eqn_blocks));
   12.26 -      val (simp_thms, thy'') = PureThy.add_thms simps thy';
   12.27 +      val simps = maps (make_simps thy') (unfold_thms ~~ eqn_blocks);
   12.28 +      val (simp_thms, thy'') = PureThy.add_thms ((map o apfst o apfst) Binding.name simps) thy';
   12.29        
   12.30        val simp_names = map (fn name => name^"_simps") cnames;
   12.31        val simp_attribute = rpair [Simplifier.simp_add];
   12.32        val simps' = map simp_attribute (simp_names ~~ unconcat lengths simp_thms);
   12.33      in
   12.34 -      (snd o PureThy.add_thmss simps') thy''
   12.35 +      (snd o PureThy.add_thmss ((map o apfst o apfst) Binding.name simps')) thy''
   12.36      end
   12.37      else thy'
   12.38    end;
   12.39 @@ -278,7 +278,7 @@
   12.40      val ts = map (prep_term thy) strings;
   12.41      val simps = map (fix_pat thy) ts;
   12.42    in
   12.43 -    (snd o PureThy.add_thmss [((Binding.base_name name, simps), atts)]) thy
   12.44 +    (snd o PureThy.add_thmss [((name, simps), atts)]) thy
   12.45    end;
   12.46  
   12.47  val add_fixpat = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
    13.1 --- a/src/HOLCF/Tools/pcpodef_package.ML	Wed Jan 21 16:51:45 2009 +0100
    13.2 +++ b/src/HOLCF/Tools/pcpodef_package.ML	Wed Jan 21 18:27:43 2009 +0100
    13.3 @@ -97,12 +97,12 @@
    13.4          theory'
    13.5          |> Sign.add_path name
    13.6          |> PureThy.add_thms
    13.7 -          ([(("adm_" ^ name, admissible'), []),
    13.8 -            (("cont_" ^ Rep_name, @{thm typedef_cont_Rep} OF cpo_thms'), []),
    13.9 -            (("cont_" ^ Abs_name, @{thm typedef_cont_Abs} OF cpo_thms'), []),
   13.10 -            (("lub_" ^ name, @{thm typedef_lub} OF cpo_thms'), []),
   13.11 -            (("thelub_" ^ name, @{thm typedef_thelub} OF cpo_thms'), []),
   13.12 -            (("compact_" ^ name, @{thm typedef_compact} OF cpo_thms'), [])])
   13.13 +          ([((Binding.name ("adm_" ^ name), admissible'), []),
   13.14 +            ((Binding.name ("cont_" ^ Rep_name), @{thm typedef_cont_Rep} OF cpo_thms'), []),
   13.15 +            ((Binding.name ("cont_" ^ Abs_name), @{thm typedef_cont_Abs} OF cpo_thms'), []),
   13.16 +            ((Binding.name ("lub_" ^ name), @{thm typedef_lub} OF cpo_thms'), []),
   13.17 +            ((Binding.name ("thelub_" ^ name), @{thm typedef_thelub} OF cpo_thms'), []),
   13.18 +            ((Binding.name ("compact_" ^ name), @{thm typedef_compact} OF cpo_thms'), [])])
   13.19          |> snd
   13.20          |> Sign.parent_path
   13.21        end;
   13.22 @@ -119,12 +119,12 @@
   13.23          theory'
   13.24          |> Sign.add_path name
   13.25          |> PureThy.add_thms
   13.26 -            ([((Rep_name ^ "_strict", @{thm typedef_Rep_strict} OF pcpo_thms'), []),
   13.27 -              ((Abs_name ^ "_strict", @{thm typedef_Abs_strict} OF pcpo_thms'), []),
   13.28 -              ((Rep_name ^ "_strict_iff", @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []),
   13.29 -              ((Abs_name ^ "_strict_iff", @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []),
   13.30 -              ((Rep_name ^ "_defined", @{thm typedef_Rep_defined} OF pcpo_thms'), []),
   13.31 -              ((Abs_name ^ "_defined", @{thm typedef_Abs_defined} OF pcpo_thms'), [])
   13.32 +            ([((Binding.name (Rep_name ^ "_strict"), @{thm typedef_Rep_strict} OF pcpo_thms'), []),
   13.33 +              ((Binding.name (Abs_name ^ "_strict"), @{thm typedef_Abs_strict} OF pcpo_thms'), []),
   13.34 +              ((Binding.name (Rep_name ^ "_strict_iff"), @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []),
   13.35 +              ((Binding.name (Abs_name ^ "_strict_iff"), @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []),
   13.36 +              ((Binding.name (Rep_name ^ "_defined"), @{thm typedef_Rep_defined} OF pcpo_thms'), []),
   13.37 +              ((Binding.name (Abs_name ^ "_defined"), @{thm typedef_Abs_defined} OF pcpo_thms'), [])
   13.38                ])
   13.39          |> snd
   13.40          |> Sign.parent_path