1.1 --- a/src/HOL/Import/proof_kernel.ML	Tue Jul 29 08:15:39 2008 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Tue Jul 29 08:15:40 2008 +0200
     1.3 @@ -1932,7 +1932,7 @@
     1.4                         Replaying _ => thy
     1.5                       | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; Sign.add_consts_i [(constname,ctype,csyn)] thy)
     1.6          val eq = mk_defeq constname rhs' thy1
     1.7 -        val (thms, thy2) = PureThy.add_defs_i false [((thmname,eq),[])] thy1
     1.8 +        val (thms, thy2) = PureThy.add_defs false [((thmname,eq),[])] thy1
     1.9          val _ = ImportRecorder.add_defs thmname eq
    1.10          val def_thm = hd thms
    1.11          val thm' = def_thm RS meta_eq_to_obj_eq_thm

     2.1 --- a/src/HOL/Import/replay.ML	Tue Jul 29 08:15:39 2008 +0200
     2.2 +++ b/src/HOL/Import/replay.ML	Tue Jul 29 08:15:40 2008 +0200
     2.3 @@ -340,7 +340,7 @@
     2.4  	  | delta (Hol_move (fullname, moved_thmname)) thy = 
     2.5  	    add_hol4_move fullname moved_thmname thy
     2.6  	  | delta (Defs (thmname, eq)) thy =
     2.7 -	    snd (PureThy.add_defs_i false [((thmname, eq), [])] thy)
     2.8 +	    snd (PureThy.add_defs false [((thmname, eq), [])] thy)
     2.9  	  | delta (Hol_theorem (thyname, thmname, th)) thy =
    2.10  	    add_hol4_theorem thyname thmname ([], th_of thy th) thy
    2.11  	  | delta (Typedef (thmname, typ, c, repabs, th)) thy = 

     3.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Jul 29 08:15:39 2008 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Jul 29 08:15:40 2008 +0200
     3.3 @@ -152,7 +152,7 @@
     3.4          val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
     3.5        in
     3.6          thy |> Sign.add_consts_i [("swap_" ^ ak_name, swapT, NoSyn)] 
     3.7 -            |> PureThy.add_defs_unchecked_i true [((name, def2),[])]
     3.8 +            |> PureThy.add_defs_unchecked true [((name, def2),[])]
     3.9              |> snd
    3.10              |> OldPrimrecPackage.add_primrec_unchecked_i "" [(("", def1),[])]
    3.11        end) ak_names_types thy1;
    3.12 @@ -207,7 +207,7 @@
    3.13            val def = Logic.mk_equals
    3.14                      (cperm $ pi $ a, if ak_name = ak_name' then cperm_def $ pi $ a else a)
    3.15          in
    3.16 -          PureThy.add_defs_unchecked_i true [((name, def),[])] thy'
    3.17 +          PureThy.add_defs_unchecked true [((name, def),[])] thy'
    3.18          end) ak_names_types thy) ak_names_types thy4;
    3.19      
    3.20      (* proves that every atom-kind is an instance of at *)

     4.1 --- a/src/HOL/Nominal/nominal_package.ML	Tue Jul 29 08:15:39 2008 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_package.ML	Tue Jul 29 08:15:40 2008 +0200
     4.3 @@ -617,7 +617,7 @@
     4.4            val tvs' = map (fn s => TFree (s, the (AList.lookup op = sorts' s))) tvs;
     4.5            val T = Type (Sign.intern_type thy name, tvs');
     4.6          in apfst (pair r o hd)
     4.7 -          (PureThy.add_defs_unchecked_i true [(("prm_" ^ name ^ "_def", Logic.mk_equals
     4.8 +          (PureThy.add_defs_unchecked true [(("prm_" ^ name ^ "_def", Logic.mk_equals
     4.9              (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
    4.10               Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $
    4.11                 (Const ("Nominal.perm", permT --> U --> U) $ pi $
    4.12 @@ -783,7 +783,7 @@
    4.13          val def_name = (Sign.base_name cname) ^ "_def";
    4.14          val ([def_thm], thy') = thy |>
    4.15            Sign.add_consts_i [(cname', constrT, mx)] |>
    4.16 -          (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)]
    4.17 +          (PureThy.add_defs false o map Thm.no_attributes) [(def_name, def)]
    4.18        in (thy', defs @ [def_thm], eqns @ [eqn]) end;
    4.19  
    4.20      fun dt_constr_defs ((thy, defs, eqns, dist_lemmas), ((((((_, (_, _, constrs)),
    4.21 @@ -1965,7 +1965,7 @@
    4.22        |> Sign.add_consts_i (map (fn ((name, T), T') =>
    4.23            (Sign.base_name name, rec_fn_Ts @ [T] ---> T', NoSyn))
    4.24            (reccomb_names ~~ recTs ~~ rec_result_Ts))
    4.25 -      |> (PureThy.add_defs_i false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
    4.26 +      |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
    4.27            ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T,
    4.28             Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
    4.29               set $ Free ("x", T) $ Free ("y", T'))))))

     5.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Tue Jul 29 08:15:39 2008 +0200
     5.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Tue Jul 29 08:15:40 2008 +0200
     5.3 @@ -391,9 +391,9 @@
     5.4  fun thy_note ((name, atts), thms) =
     5.5    PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
     5.6  fun thy_def false ((name, atts), t) =
     5.7 -      PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm))
     5.8 +      PureThy.add_defs false [((name, t), atts)] #-> (fn [thm] => pair (name, thm))
     5.9    | thy_def true ((name, atts), t) =
    5.10 -      PureThy.add_defs_unchecked_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
    5.11 +      PureThy.add_defs_unchecked false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
    5.12  
    5.13  in
    5.14  

     6.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Tue Jul 29 08:15:39 2008 +0200
     6.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Tue Jul 29 08:15:40 2008 +0200
     6.3 @@ -671,7 +671,7 @@
     6.4  
     6.5  setup {*
     6.6  Theory.add_consts_i const_decls
     6.7 -#> (fn thy  => let val ([thm],thy') = PureThy.add_axioms_i [(("dist_axiom",dist),[])] thy
     6.8 +#> (fn thy  => let val ([thm],thy') = PureThy.add_axioms [(("dist_axiom",dist),[])] thy
     6.9                 in (da := thm; thy') end)
    6.10  *}
    6.11  

     7.1 --- a/src/HOL/Tools/TFL/tfl.ML	Tue Jul 29 08:15:39 2008 +0200
     7.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Tue Jul 29 08:15:40 2008 +0200
     7.3 @@ -392,7 +392,7 @@
     7.4                            (wfrec $ map_types poly_tvars R)
     7.5                        $ functional
     7.6       val def_term = mk_const_def thy (x, Ty, wfrec_R_M)
     7.7 -     val ([def], thy') = PureThy.add_defs_i false [Thm.no_attributes (def_name, def_term)] thy
     7.8 +     val ([def], thy') = PureThy.add_defs false [Thm.no_attributes (def_name, def_term)] thy
     7.9   in (thy', def) end;
    7.10  end;
    7.11  
    7.12 @@ -550,7 +550,7 @@
    7.13       val defn = mk_const_def thy (name, Ty, S.list_mk_abs (args,rhs))
    7.14       val ([def0], theory) =
    7.15         thy
    7.16 -       |> PureThy.add_defs_i false
    7.17 +       |> PureThy.add_defs false
    7.18              [Thm.no_attributes (fid ^ "_def", defn)]
    7.19       val def = Thm.freezeT def0;
    7.20       val dummy = if !trace then writeln ("DEF = " ^ Display.string_of_thm def)

     8.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Jul 29 08:15:39 2008 +0200
     8.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Jul 29 08:15:40 2008 +0200
     8.3 @@ -239,7 +239,7 @@
     8.4        |> Sign.add_consts_i (map (fn ((name, T), T') =>
     8.5            (Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
     8.6            (reccomb_names ~~ recTs ~~ rec_result_Ts))
     8.7 -      |> (PureThy.add_defs_i false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
     8.8 +      |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
     8.9            ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T,
    8.10             Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
    8.11               set $ Free ("x", T) $ Free ("y", T'))))))
    8.12 @@ -323,7 +323,7 @@
    8.13            val ([def_thm], thy') =
    8.14              thy
    8.15              |> Sign.declare_const [] decl |> snd
    8.16 -            |> (PureThy.add_defs_i false o map Thm.no_attributes) [def];
    8.17 +            |> (PureThy.add_defs false o map Thm.no_attributes) [def];
    8.18  
    8.19          in (defs @ [def_thm], thy')
    8.20          end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~

     9.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jul 29 08:15:39 2008 +0200
     9.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jul 29 08:15:40 2008 +0200
     9.3 @@ -244,7 +244,7 @@
     9.4          val ([def_thm], thy') =
     9.5            thy
     9.6            |> Sign.add_consts_i [(cname', constrT, mx)]
     9.7 -          |> (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)];
     9.8 +          |> (PureThy.add_defs false o map Thm.no_attributes) [(def_name, def)];
     9.9  
    9.10        in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
    9.11  
    9.12 @@ -348,7 +348,7 @@
    9.13          val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def",
    9.14            Logic.mk_equals (Const (iso_name, T --> Univ_elT),
    9.15              list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos);
    9.16 -        val (def_thms, thy') = (PureThy.add_defs_i false o map Thm.no_attributes) defs thy;
    9.17 +        val (def_thms, thy') = (PureThy.add_defs false o map Thm.no_attributes) defs thy;
    9.18  
    9.19          (* prove characteristic equations *)
    9.20  

    10.1 --- a/src/HOL/Tools/function_package/size.ML	Tue Jul 29 08:15:39 2008 +0200
    10.2 +++ b/src/HOL/Tools/function_package/size.ML	Tue Jul 29 08:15:40 2008 +0200
    10.3 @@ -143,7 +143,7 @@
    10.4        |> Sign.add_consts_i (map (fn (s, T) =>
    10.5             (Sign.base_name s, param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
    10.6             (size_names ~~ recTs1))
    10.7 -      |> PureThy.add_defs_i false
    10.8 +      |> PureThy.add_defs false
    10.9          (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
   10.10             (def_names ~~ (size_fns ~~ rec_combs1)))
   10.11        ||> TheoryTarget.instantiation

    11.1 --- a/src/HOL/Tools/old_primrec_package.ML	Tue Jul 29 08:15:39 2008 +0200
    11.2 +++ b/src/HOL/Tools/old_primrec_package.ML	Tue Jul 29 08:15:40 2008 +0200
    11.3 @@ -308,9 +308,9 @@
    11.4  fun thy_note ((name, atts), thms) =
    11.5    PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
    11.6  fun thy_def false ((name, atts), t) =
    11.7 -      PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm))
    11.8 +      PureThy.add_defs false [((name, t), atts)] #-> (fn [thm] => pair (name, thm))
    11.9    | thy_def true ((name, atts), t) =
   11.10 -      PureThy.add_defs_unchecked_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
   11.11 +      PureThy.add_defs_unchecked false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
   11.12  
   11.13  in
   11.14  

    12.1 --- a/src/HOL/Tools/record_package.ML	Tue Jul 29 08:15:39 2008 +0200
    12.2 +++ b/src/HOL/Tools/record_package.ML	Tue Jul 29 08:15:40 2008 +0200
    12.3 @@ -1540,8 +1540,8 @@
    12.4        |> extension_typedef name repT (alphas@[zeta])
    12.5        ||> Sign.add_consts_i
    12.6              (map Syntax.no_syn ((apfst base ext_decl)::dest_decls@upd_decls))
    12.7 -      ||>> PureThy.add_defs_i false (map Thm.no_attributes (ext_spec::dest_specs))
    12.8 -      ||>> PureThy.add_defs_i false (map Thm.no_attributes upd_specs)
    12.9 +      ||>> PureThy.add_defs false (map Thm.no_attributes (ext_spec::dest_specs))
   12.10 +      ||>> PureThy.add_defs false (map Thm.no_attributes upd_specs)
   12.11        |-> (fn args as ((_, dest_defs), upd_defs) =>
   12.12            fold Code.add_default_func dest_defs
   12.13            #> fold Code.add_default_func upd_defs
   12.14 @@ -1944,9 +1944,9 @@
   12.15            (map2 (fn (x, T) => fn mx => (x, T, mx)) sel_decls (field_syntax @ [Syntax.NoSyn]))
   12.16        |> (Sign.add_consts_i o map Syntax.no_syn)
   12.17            (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
   12.18 -      |> ((PureThy.add_defs_i false o map Thm.no_attributes) sel_specs)
   12.19 -      ||>> ((PureThy.add_defs_i false o map Thm.no_attributes) upd_specs)
   12.20 -      ||>> ((PureThy.add_defs_i false o map Thm.no_attributes)
   12.21 +      |> ((PureThy.add_defs false o map Thm.no_attributes) sel_specs)
   12.22 +      ||>> ((PureThy.add_defs false o map Thm.no_attributes) upd_specs)
   12.23 +      ||>> ((PureThy.add_defs false o map Thm.no_attributes)
   12.24               [make_spec, fields_spec, extend_spec, truncate_spec])
   12.25        |-> (fn defs as ((sel_defs, upd_defs), derived_defs) =>
   12.26            fold Code.add_default_func sel_defs

    13.1 --- a/src/HOL/Tools/specification_package.ML	Tue Jul 29 08:15:39 2008 +0200
    13.2 +++ b/src/HOL/Tools/specification_package.ML	Tue Jul 29 08:15:40 2008 +0200
    13.3 @@ -29,7 +29,7 @@
    13.4                                 else thname
    13.5                  val def_eq = Logic.mk_equals (Const(cname_full,ctype),
    13.6                                                HOLogic.choice_const ctype $  P)
    13.7 -                val (thms, thy') = PureThy.add_defs_i covld [((cdefname,def_eq),[])] thy
    13.8 +                val (thms, thy') = PureThy.add_defs covld [((cdefname,def_eq),[])] thy
    13.9                  val thm' = [thm,hd thms] MRS @{thm exE_some}
   13.10              in
   13.11                  mk_definitional cos (thy',thm')
   13.12 @@ -40,7 +40,7 @@
   13.13          let
   13.14              fun process [] (thy,tm) =
   13.15                  let
   13.16 -                    val (thms, thy') = PureThy.add_axioms_i [((axname,HOLogic.mk_Trueprop tm),[])] thy
   13.17 +                    val (thms, thy') = PureThy.add_axioms [((axname,HOLogic.mk_Trueprop tm),[])] thy
   13.18                  in
   13.19                      (thy',hd thms)
   13.20                  end

    14.1 --- a/src/HOL/Tools/typedef_package.ML	Tue Jul 29 08:15:39 2008 +0200
    14.2 +++ b/src/HOL/Tools/typedef_package.ML	Tue Jul 29 08:15:40 2008 +0200
    14.3 @@ -128,7 +128,7 @@
    14.4      fun add_def eq thy =
    14.5        if def then
    14.6          thy
    14.7 -        |> PureThy.add_defs_i false [Thm.no_attributes eq]
    14.8 +        |> PureThy.add_defs false [Thm.no_attributes eq]
    14.9          |-> (fn [th] => pair (SOME th))
   14.10        else (NONE, thy);
   14.11  
   14.12 @@ -140,7 +140,7 @@
   14.13          [(Rep_name, newT --> oldT, NoSyn),
   14.14           (Abs_name, oldT --> newT, NoSyn)])
   14.15        #> add_def (PrimitiveDefs.mk_defpair (setC, set))
   14.16 -      ##>> PureThy.add_axioms_i [((typedef_name, typedef_prop),
   14.17 +      ##>> PureThy.add_axioms [((typedef_name, typedef_prop),
   14.18            [apsnd (fn cond_axm => nonempty RS cond_axm)])]
   14.19        ##> Theory.add_deps "" (dest_Const RepC) typedef_deps
   14.20        ##> Theory.add_deps "" (dest_Const AbsC) typedef_deps

    15.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Tue Jul 29 08:15:39 2008 +0200
    15.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Tue Jul 29 08:15:40 2008 +0200
    15.3 @@ -350,7 +350,7 @@
    15.4  (automaton_name ^ "_trans",
    15.5   "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
    15.6  (automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
    15.7 -|> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
    15.8 +|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
    15.9  [(automaton_name ^ "_initial_def",
   15.10  automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
   15.11  (automaton_name ^ "_asig_def",
   15.12 @@ -391,7 +391,7 @@
   15.13    Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
   15.14     Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
   15.15  ,NoSyn)]
   15.16 -|> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
   15.17 +|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
   15.18  [(automaton_name ^ "_def",
   15.19  automaton_name ^ " == " ^ comp_list)]
   15.20  end)
   15.21 @@ -406,7 +406,7 @@
   15.22  thy
   15.23  |> ContConsts.add_consts_i
   15.24  [(automaton_name, auttyp,NoSyn)]
   15.25 -|> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
   15.26 +|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
   15.27  [(automaton_name ^ "_def",
   15.28  automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] 
   15.29  end)
   15.30 @@ -420,7 +420,7 @@
   15.31  thy
   15.32  |> ContConsts.add_consts_i
   15.33  [(automaton_name, auttyp,NoSyn)]
   15.34 -|> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
   15.35 +|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
   15.36  [(automaton_name ^ "_def",
   15.37  automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] 
   15.38  end)
   15.39 @@ -446,7 +446,7 @@
   15.40    Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
   15.41     Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
   15.42  ,NoSyn)]
   15.43 -|> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
   15.44 +|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
   15.45  [(automaton_name ^ "_def",
   15.46  automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
   15.47  end)

    16.1 --- a/src/HOLCF/Tools/domain/domain_axioms.ML	Tue Jul 29 08:15:39 2008 +0200
    16.2 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML	Tue Jul 29 08:15:40 2008 +0200
    16.3 @@ -111,10 +111,10 @@
    16.4  
    16.5  fun infer_props thy = map (apsnd (FixrecPackage.legacy_infer_prop thy));
    16.6  
    16.7 -fun add_axioms_i x = snd o PureThy.add_axioms_i (map Thm.no_attributes x);
    16.8 +fun add_axioms_i x = snd o PureThy.add_axioms (map Thm.no_attributes x);
    16.9  fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy;
   16.10  
   16.11 -fun add_defs_i x = snd o (PureThy.add_defs_i false) (map Thm.no_attributes x);
   16.12 +fun add_defs_i x = snd o (PureThy.add_defs false) (map Thm.no_attributes x);
   16.13  fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
   16.14  
   16.15  in (* local *)

    17.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Tue Jul 29 08:15:39 2008 +0200
    17.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Tue Jul 29 08:15:40 2008 +0200
    17.3 @@ -97,7 +97,7 @@
    17.4      
    17.5      val fixdefs = map (apsnd (legacy_infer_prop thy)) pre_fixdefs;
    17.6      val (fixdef_thms, thy') =
    17.7 -      PureThy.add_defs_i false (map Thm.no_attributes fixdefs) thy;
    17.8 +      PureThy.add_defs false (map Thm.no_attributes fixdefs) thy;
    17.9      val ctuple_fixdef_thm = foldr1 (fn (x,y) => @{thm cpair_equalI} OF [x,y]) fixdef_thms;
   17.10      
   17.11      val ctuple_unfold = legacy_infer_term thy' (mk_trp (mk_ctuple lhss === mk_ctuple rhss));

    18.1 --- a/src/HOLCF/Tools/pcpodef_package.ML	Tue Jul 29 08:15:39 2008 +0200
    18.2 +++ b/src/HOLCF/Tools/pcpodef_package.ML	Tue Jul 29 08:15:40 2008 +0200
    18.3 @@ -90,7 +90,7 @@
    18.4        |> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac
    18.5        ||> AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.sq_ord"])
    18.6             (Class.intro_classes_tac [])
    18.7 -      ||>> PureThy.add_defs_i true [Thm.no_attributes less_def]
    18.8 +      ||>> PureThy.add_defs true [Thm.no_attributes less_def]
    18.9        |-> (fn ((_, {type_definition, set_def, ...}), [less_definition]) =>
   18.10            AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.po"])
   18.11               (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1)

    19.1 --- a/src/Pure/Isar/constdefs.ML	Tue Jul 29 08:15:39 2008 +0200
    19.2 +++ b/src/Pure/Isar/constdefs.ML	Tue Jul 29 08:15:40 2008 +0200
    19.3 @@ -50,7 +50,7 @@
    19.4      val thy' =
    19.5        thy
    19.6        |> Sign.add_consts_i [(c, T, mx)]
    19.7 -      |> PureThy.add_defs_i false [((name, def), atts)]
    19.8 +      |> PureThy.add_defs false [((name, def), atts)]
    19.9        |-> (fn [thm] => Code.add_default_func thm);
   19.10    in ((c, T), thy') end;
   19.11  

    20.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Jul 29 08:15:39 2008 +0200
    20.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Jul 29 08:15:40 2008 +0200
    20.3 @@ -192,20 +192,20 @@
    20.4  fun add_axms f args thy =
    20.5    f (map (fn (x, srcs) => (x, map (Attrib.attribute thy) srcs)) args) thy;
    20.6  
    20.7 -val add_axioms = add_axms (snd oo PureThy.add_axioms);
    20.8 +val add_axioms = add_axms (snd oo PureThy.add_axioms_cmd);
    20.9  
   20.10  fun add_defs ((unchecked, overloaded), args) =
   20.11    add_axms
   20.12 -    (snd oo (if unchecked then PureThy.add_defs_unchecked else PureThy.add_defs) overloaded) args;
   20.13 +    (snd oo (if unchecked then PureThy.add_defs_unchecked_cmd else PureThy.add_defs_cmd) overloaded) args;
   20.14  
   20.15  
   20.16  (* facts *)
   20.17  
   20.18  fun apply_theorems args thy =
   20.19    let val facts = Attrib.map_facts (Attrib.attribute thy) [(("", []), args)]
   20.20 -  in apfst (maps snd) (PureThy.note_thmss "" facts thy) end;
   20.21 +  in apfst (maps snd) (PureThy.note_thmss_cmd "" facts thy) end;
   20.22  
   20.23 -fun apply_theorems_i args = apfst (maps snd) o PureThy.note_thmss_i "" [(("", []), args)];
   20.24 +fun apply_theorems_i args = apfst (maps snd) o PureThy.note_thmss "" [(("", []), args)];
   20.25  
   20.26  
   20.27  (* declarations *)

    21.1 --- a/src/Pure/Proof/extraction.ML	Tue Jul 29 08:15:39 2008 +0200
    21.2 +++ b/src/Pure/Proof/extraction.ML	Tue Jul 29 08:15:40 2008 +0200
    21.3 @@ -729,7 +729,7 @@
    21.4               val (def_thms, thy') = if t = nullt then ([], thy) else
    21.5                 thy
    21.6                 |> Sign.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)]
    21.7 -               |> PureThy.add_defs_i false [((extr_name s vs ^ "_def",
    21.8 +               |> PureThy.add_defs false [((extr_name s vs ^ "_def",
    21.9                      Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
   21.10             in
   21.11               thy'

    22.1 --- a/src/Pure/axclass.ML	Tue Jul 29 08:15:39 2008 +0200
    22.2 +++ b/src/Pure/axclass.ML	Tue Jul 29 08:15:40 2008 +0200
    22.3 @@ -468,7 +468,7 @@
    22.4      val ([def], def_thy) =
    22.5        thy
    22.6        |> Sign.primitive_class (bclass, super)
    22.7 -      |> PureThy.add_defs_i false [((Thm.def_name bconst, class_eq), [])];
    22.8 +      |> PureThy.add_defs false [((Thm.def_name bconst, class_eq), [])];
    22.9      val (raw_intro, (raw_classrel, raw_axioms)) =
   22.10        split_defined (length conjs) def ||> chop (length super);
   22.11  
   22.12 @@ -478,10 +478,13 @@
   22.13      val class_triv = Thm.class_triv def_thy class;
   22.14      val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) =
   22.15        def_thy
   22.16 -      |> PureThy.note_thmss_qualified "" bconst
   22.17 +      |> Sign.add_path bconst
   22.18 +      |> Sign.no_base_names
   22.19 +      |> PureThy.note_thmss ""
   22.20          [((introN, []), [([Drule.standard raw_intro], [])]),
   22.21           ((superN, []), [(map Drule.standard raw_classrel, [])]),
   22.22 -         ((axiomsN, []), [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])];
   22.23 +         ((axiomsN, []), [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]
   22.24 +      ||> Sign.restore_naming def_thy;
   22.25  
   22.26  
   22.27      (* result *)
   22.28 @@ -491,7 +494,7 @@
   22.29        facts_thy
   22.30        |> fold put_classrel (map (pair class) super ~~ classrel)
   22.31        |> Sign.add_path bconst
   22.32 -      |> PureThy.note_thmss_i "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd
   22.33 +      |> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd
   22.34        |> Sign.restore_naming facts_thy
   22.35        |> map_axclasses (fn (axclasses, parameters) =>
   22.36          (Symtab.update (class, axclass) axclasses,
   22.37 @@ -510,7 +513,7 @@
   22.38      val args = prep thy raw_args;
   22.39      val specs = mk args;
   22.40      val names = name args;
   22.41 -  in thy |> PureThy.add_axioms_i (map (rpair []) (names ~~ specs)) |-> fold add end;
   22.42 +  in thy |> PureThy.add_axioms (map (rpair []) (names ~~ specs)) |-> fold add end;
   22.43  
   22.44  fun ax_classrel prep =
   22.45    axiomatize (map o prep) (map Logic.mk_classrel)

    23.1 --- a/src/Pure/pure_thy.ML	Tue Jul 29 08:15:39 2008 +0200
    23.2 +++ b/src/Pure/pure_thy.ML	Tue Jul 29 08:15:40 2008 +0200
    23.3 @@ -43,27 +43,25 @@
    23.4    val store_thms: bstring * thm list -> theory -> thm list * theory
    23.5    val store_thm: bstring * thm -> theory -> thm * theory
    23.6    val store_thm_open: bstring * thm -> theory -> thm * theory
    23.7 +  val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory
    23.8    val add_thm: (bstring * thm) * attribute list -> theory -> thm * theory
    23.9 -  val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory
   23.10    val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory
   23.11    val add_thms_dynamic: bstring * (Context.generic -> thm list) -> theory -> theory
   23.12    val note_thmss: string -> ((bstring * attribute list) *
   23.13 -    (Facts.ref * attribute list) list) list -> theory -> (bstring * thm list) list * theory
   23.14 -  val note_thmss_i: string -> ((bstring * attribute list) *
   23.15      (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory
   23.16    val note_thmss_grouped: string -> string -> ((bstring * attribute list) *
   23.17      (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory
   23.18 -  val note_thmss_qualified: string -> string -> ((bstring * attribute list) *
   23.19 -    (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory
   23.20 -  val add_axioms: ((bstring * string) * attribute list) list -> theory -> thm list * theory
   23.21 -  val add_axioms_i: ((bstring * term) * attribute list) list -> theory -> thm list * theory
   23.22 -  val add_defs: bool -> ((bstring * string) * attribute list) list ->
   23.23 +  val note_thmss_cmd: string -> ((bstring * attribute list) *
   23.24 +    (Facts.ref * attribute list) list) list -> theory -> (bstring * thm list) list * theory
   23.25 +  val add_axioms: ((bstring * term) * attribute list) list -> theory -> thm list * theory
   23.26 +  val add_axioms_cmd: ((bstring * string) * attribute list) list -> theory -> thm list * theory
   23.27 +  val add_defs: bool -> ((bstring * term) * attribute list) list ->
   23.28      theory -> thm list * theory
   23.29 -  val add_defs_i: bool -> ((bstring * term) * attribute list) list ->
   23.30 +  val add_defs_unchecked: bool -> ((bstring * term) * attribute list) list ->
   23.31      theory -> thm list * theory
   23.32 -  val add_defs_unchecked: bool -> ((bstring * string) * attribute list) list ->
   23.33 +  val add_defs_unchecked_cmd: bool -> ((bstring * string) * attribute list) list ->
   23.34      theory -> thm list * theory
   23.35 -  val add_defs_unchecked_i: bool -> ((bstring * term) * attribute list) list ->
   23.36 +  val add_defs_cmd: bool -> ((bstring * string) * attribute list) list ->
   23.37      theory -> thm list * theory
   23.38    val old_appl_syntax: theory -> bool
   23.39    val old_appl_syntax_setup: theory -> theory
   23.40 @@ -252,19 +250,12 @@
   23.41  
   23.42  in
   23.43  
   23.44 -fun note_thmss k = gen_note_thmss (fn thy => get_fact (Context.Theory thy) thy) (kind k);
   23.45 -fun note_thmss_i k = gen_note_thmss (K I) (kind k);
   23.46 +fun note_thmss k = gen_note_thmss (K I) (kind k);
   23.47  fun note_thmss_grouped k g = gen_note_thmss (K I) (kind k #> group g);
   23.48 +fun note_thmss_cmd k = gen_note_thmss (fn thy => get_fact (Context.Theory thy) thy) (kind k);
   23.49  
   23.50  end;
   23.51  
   23.52 -fun note_thmss_qualified k path facts thy =
   23.53 -  thy
   23.54 -  |> Sign.add_path path
   23.55 -  |> Sign.no_base_names
   23.56 -  |> note_thmss_i k facts
   23.57 -  ||> Sign.restore_naming thy;
   23.58 -
   23.59  
   23.60  (* store axioms as theorems *)
   23.61  
   23.62 @@ -278,12 +269,12 @@
   23.63        val thm = hd (get_axs thy' named_ax);
   23.64      in apfst hd (gen_add_thms (K I) [((name, thm), atts)] thy') end);
   23.65  in
   23.66 -  val add_axioms           = add_axm Theory.add_axioms;
   23.67 -  val add_axioms_i         = add_axm Theory.add_axioms_i;
   23.68 -  val add_defs             = add_axm o Theory.add_defs false;
   23.69 -  val add_defs_i           = add_axm o Theory.add_defs_i false;
   23.70 -  val add_defs_unchecked   = add_axm o Theory.add_defs true;
   23.71 -  val add_defs_unchecked_i = add_axm o Theory.add_defs_i true;
   23.72 +  val add_defs               = add_axm o Theory.add_defs_i false;
   23.73 +  val add_defs_unchecked     = add_axm o Theory.add_defs_i true;
   23.74 +  val add_axioms             = add_axm Theory.add_axioms_i;
   23.75 +  val add_defs_cmd           = add_axm o Theory.add_defs false;
   23.76 +  val add_defs_unchecked_cmd = add_axm o Theory.add_defs true;
   23.77 +  val add_axioms_cmd         = add_axm Theory.add_axioms;
   23.78  end;
   23.79  
   23.80  
   23.81 @@ -414,7 +405,7 @@
   23.82    #> Sign.add_consts_i
   23.83     [("term", typ "'a => prop", NoSyn),
   23.84      ("conjunction", typ "prop => prop => prop", NoSyn)]
   23.85 -  #> (add_defs_i false o map Thm.no_attributes)
   23.86 +  #> (add_defs false o map Thm.no_attributes)
   23.87     [("prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
   23.88      ("term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
   23.89      ("conjunction_def", prop "(A && B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd

    24.1 --- a/src/ZF/Tools/datatype_package.ML	Tue Jul 29 08:15:39 2008 +0200
    24.2 +++ b/src/ZF/Tools/datatype_package.ML	Tue Jul 29 08:15:40 2008 +0200
    24.3 @@ -247,14 +247,14 @@
    24.4        if need_recursor then
    24.5             thy |> Sign.add_consts_i
    24.6                      [(recursor_base_name, recursor_typ, NoSyn)]
    24.7 -               |> (snd o PureThy.add_defs_i false [Thm.no_attributes recursor_def])
    24.8 +               |> (snd o PureThy.add_defs false [Thm.no_attributes recursor_def])
    24.9        else thy;
   24.10  
   24.11    val (con_defs, thy0) = thy_path
   24.12               |> Sign.add_consts_i
   24.13                   ((case_base_name, case_typ, NoSyn) ::
   24.14                    map #1 (List.concat con_ty_lists))
   24.15 -             |> PureThy.add_defs_i false
   24.16 +             |> PureThy.add_defs false
   24.17                   (map Thm.no_attributes
   24.18                    (case_def ::
   24.19                     List.concat (ListPair.map mk_con_defs

    25.1 --- a/src/ZF/Tools/ind_cases.ML	Tue Jul 29 08:15:39 2008 +0200
    25.2 +++ b/src/ZF/Tools/ind_cases.ML	Tue Jul 29 08:15:40 2008 +0200
    25.3 @@ -52,7 +52,7 @@
    25.4      val facts = args |> map (fn ((name, srcs), props) =>
    25.5        ((name, map (Attrib.attribute thy) srcs),
    25.6          map (Thm.no_attributes o single o mk_cases) props));
    25.7 -  in thy |> PureThy.note_thmss_i "" facts |> snd end;
    25.8 +  in thy |> PureThy.note_thmss "" facts |> snd end;
    25.9  
   25.10  
   25.11  (* ind_cases method *)

    26.1 --- a/src/ZF/Tools/inductive_package.ML	Tue Jul 29 08:15:39 2008 +0200
    26.2 +++ b/src/ZF/Tools/inductive_package.ML	Tue Jul 29 08:15:40 2008 +0200
    26.3 @@ -174,7 +174,7 @@
    26.4    val (_, thy1) =
    26.5      thy
    26.6      |> Sign.add_path big_rec_base_name
    26.7 -    |> PureThy.add_defs_i false (map Thm.no_attributes axpairs);
    26.8 +    |> PureThy.add_defs false (map Thm.no_attributes axpairs);
    26.9  
   26.10    val ctxt1 = ProofContext.init thy1;
   26.11  

    27.1 --- a/src/ZF/Tools/primrec_package.ML	Tue Jul 29 08:15:39 2008 +0200
    27.2 +++ b/src/ZF/Tools/primrec_package.ML	Tue Jul 29 08:15:40 2008 +0200
    27.3 @@ -170,7 +170,7 @@
    27.4  
    27.5      val ([def_thm], thy1) = thy
    27.6        |> Sign.add_path (Sign.base_name fname)
    27.7 -      |> (PureThy.add_defs_i false o map Thm.no_attributes) [def];
    27.8 +      |> (PureThy.add_defs false o map Thm.no_attributes) [def];
    27.9  
   27.10      val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
   27.11      val eqn_thms =