# HG changeset patch
# User haftmann
# Date 1217312140 -7200
# Node ID ce171cbd4b93466346a2d77997b36afd3cfa1b5e
# Parent  24738db98d34963d852864230bb8810c778099a8
PureThy: dropped note_thmss_qualified, dropped _i suffix

diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -1932,7 +1932,7 @@
                        Replaying _ => thy
                      | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; Sign.add_consts_i [(constname,ctype,csyn)] thy)
         val eq = mk_defeq constname rhs' thy1
-        val (thms, thy2) = PureThy.add_defs_i false [((thmname,eq),[])] thy1
+        val (thms, thy2) = PureThy.add_defs false [((thmname,eq),[])] thy1
         val _ = ImportRecorder.add_defs thmname eq
         val def_thm = hd thms
         val thm' = def_thm RS meta_eq_to_obj_eq_thm
diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Import/replay.ML
--- a/src/HOL/Import/replay.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Import/replay.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -340,7 +340,7 @@
 	  | delta (Hol_move (fullname, moved_thmname)) thy = 
 	    add_hol4_move fullname moved_thmname thy
 	  | delta (Defs (thmname, eq)) thy =
-	    snd (PureThy.add_defs_i false [((thmname, eq), [])] thy)
+	    snd (PureThy.add_defs false [((thmname, eq), [])] thy)
 	  | delta (Hol_theorem (thyname, thmname, th)) thy =
 	    add_hol4_theorem thyname thmname ([], th_of thy th) thy
 	  | delta (Typedef (thmname, typ, c, repabs, th)) thy = 
diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -152,7 +152,7 @@
         val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
       in
         thy |> Sign.add_consts_i [("swap_" ^ ak_name, swapT, NoSyn)] 
-            |> PureThy.add_defs_unchecked_i true [((name, def2),[])]
+            |> PureThy.add_defs_unchecked true [((name, def2),[])]
             |> snd
             |> OldPrimrecPackage.add_primrec_unchecked_i "" [(("", def1),[])]
       end) ak_names_types thy1;
@@ -207,7 +207,7 @@
           val def = Logic.mk_equals
                     (cperm $ pi $ a, if ak_name = ak_name' then cperm_def $ pi $ a else a)
         in
-          PureThy.add_defs_unchecked_i true [((name, def),[])] thy'
+          PureThy.add_defs_unchecked true [((name, def),[])] thy'
         end) ak_names_types thy) ak_names_types thy4;
     
     (* proves that every atom-kind is an instance of at *)
diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -617,7 +617,7 @@
           val tvs' = map (fn s => TFree (s, the (AList.lookup op = sorts' s))) tvs;
           val T = Type (Sign.intern_type thy name, tvs');
         in apfst (pair r o hd)
-          (PureThy.add_defs_unchecked_i true [(("prm_" ^ name ^ "_def", Logic.mk_equals
+          (PureThy.add_defs_unchecked true [(("prm_" ^ name ^ "_def", Logic.mk_equals
             (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
              Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $
                (Const ("Nominal.perm", permT --> U --> U) $ pi $
@@ -783,7 +783,7 @@
         val def_name = (Sign.base_name cname) ^ "_def";
         val ([def_thm], thy') = thy |>
           Sign.add_consts_i [(cname', constrT, mx)] |>
-          (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)]
+          (PureThy.add_defs false o map Thm.no_attributes) [(def_name, def)]
       in (thy', defs @ [def_thm], eqns @ [eqn]) end;
 
     fun dt_constr_defs ((thy, defs, eqns, dist_lemmas), ((((((_, (_, _, constrs)),
@@ -1965,7 +1965,7 @@
       |> Sign.add_consts_i (map (fn ((name, T), T') =>
           (Sign.base_name name, rec_fn_Ts @ [T] ---> T', NoSyn))
           (reccomb_names ~~ recTs ~~ rec_result_Ts))
-      |> (PureThy.add_defs_i false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
+      |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
           ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T,
            Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
              set $ Free ("x", T) $ Free ("y", T'))))))
diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -391,9 +391,9 @@
 fun thy_note ((name, atts), thms) =
   PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
 fun thy_def false ((name, atts), t) =
-      PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm))
+      PureThy.add_defs false [((name, t), atts)] #-> (fn [thm] => pair (name, thm))
   | thy_def true ((name, atts), t) =
-      PureThy.add_defs_unchecked_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
+      PureThy.add_defs_unchecked false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
 
 in
 
diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Statespace/DistinctTreeProver.thy
--- a/src/HOL/Statespace/DistinctTreeProver.thy	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Statespace/DistinctTreeProver.thy	Tue Jul 29 08:15:40 2008 +0200
@@ -671,7 +671,7 @@
 
 setup {*
 Theory.add_consts_i const_decls
-#> (fn thy  => let val ([thm],thy') = PureThy.add_axioms_i [(("dist_axiom",dist),[])] thy
+#> (fn thy  => let val ([thm],thy') = PureThy.add_axioms [(("dist_axiom",dist),[])] thy
                in (da := thm; thy') end)
 *}
 
diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -392,7 +392,7 @@
                           (wfrec $ map_types poly_tvars R)
                       $ functional
      val def_term = mk_const_def thy (x, Ty, wfrec_R_M)
-     val ([def], thy') = PureThy.add_defs_i false [Thm.no_attributes (def_name, def_term)] thy
+     val ([def], thy') = PureThy.add_defs false [Thm.no_attributes (def_name, def_term)] thy
  in (thy', def) end;
 end;
 
@@ -550,7 +550,7 @@
      val defn = mk_const_def thy (name, Ty, S.list_mk_abs (args,rhs))
      val ([def0], theory) =
        thy
-       |> PureThy.add_defs_i false
+       |> PureThy.add_defs false
             [Thm.no_attributes (fid ^ "_def", defn)]
      val def = Thm.freezeT def0;
      val dummy = if !trace then writeln ("DEF = " ^ Display.string_of_thm def)
diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -239,7 +239,7 @@
       |> Sign.add_consts_i (map (fn ((name, T), T') =>
           (Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
           (reccomb_names ~~ recTs ~~ rec_result_Ts))
-      |> (PureThy.add_defs_i false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
+      |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
           ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T,
            Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
              set $ Free ("x", T) $ Free ("y", T'))))))
@@ -323,7 +323,7 @@
           val ([def_thm], thy') =
             thy
             |> Sign.declare_const [] decl |> snd
-            |> (PureThy.add_defs_i false o map Thm.no_attributes) [def];
+            |> (PureThy.add_defs false o map Thm.no_attributes) [def];
 
         in (defs @ [def_thm], thy')
         end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -244,7 +244,7 @@
         val ([def_thm], thy') =
           thy
           |> Sign.add_consts_i [(cname', constrT, mx)]
-          |> (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)];
+          |> (PureThy.add_defs false o map Thm.no_attributes) [(def_name, def)];
 
       in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
 
@@ -348,7 +348,7 @@
         val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def",
           Logic.mk_equals (Const (iso_name, T --> Univ_elT),
             list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos);
-        val (def_thms, thy') = (PureThy.add_defs_i false o map Thm.no_attributes) defs thy;
+        val (def_thms, thy') = (PureThy.add_defs false o map Thm.no_attributes) defs thy;
 
         (* prove characteristic equations *)
 
diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Tools/function_package/size.ML
--- a/src/HOL/Tools/function_package/size.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Tools/function_package/size.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -143,7 +143,7 @@
       |> Sign.add_consts_i (map (fn (s, T) =>
            (Sign.base_name s, param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
            (size_names ~~ recTs1))
-      |> PureThy.add_defs_i false
+      |> PureThy.add_defs false
         (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
            (def_names ~~ (size_fns ~~ rec_combs1)))
       ||> TheoryTarget.instantiation
diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Tools/old_primrec_package.ML
--- a/src/HOL/Tools/old_primrec_package.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Tools/old_primrec_package.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -308,9 +308,9 @@
 fun thy_note ((name, atts), thms) =
   PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
 fun thy_def false ((name, atts), t) =
-      PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm))
+      PureThy.add_defs false [((name, t), atts)] #-> (fn [thm] => pair (name, thm))
   | thy_def true ((name, atts), t) =
-      PureThy.add_defs_unchecked_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
+      PureThy.add_defs_unchecked false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
 
 in
 
diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Tools/record_package.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -1540,8 +1540,8 @@
       |> extension_typedef name repT (alphas@[zeta])
       ||> Sign.add_consts_i
             (map Syntax.no_syn ((apfst base ext_decl)::dest_decls@upd_decls))
-      ||>> PureThy.add_defs_i false (map Thm.no_attributes (ext_spec::dest_specs))
-      ||>> PureThy.add_defs_i false (map Thm.no_attributes upd_specs)
+      ||>> PureThy.add_defs false (map Thm.no_attributes (ext_spec::dest_specs))
+      ||>> PureThy.add_defs false (map Thm.no_attributes upd_specs)
       |-> (fn args as ((_, dest_defs), upd_defs) =>
           fold Code.add_default_func dest_defs
           #> fold Code.add_default_func upd_defs
@@ -1944,9 +1944,9 @@
           (map2 (fn (x, T) => fn mx => (x, T, mx)) sel_decls (field_syntax @ [Syntax.NoSyn]))
       |> (Sign.add_consts_i o map Syntax.no_syn)
           (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
-      |> ((PureThy.add_defs_i false o map Thm.no_attributes) sel_specs)
-      ||>> ((PureThy.add_defs_i false o map Thm.no_attributes) upd_specs)
-      ||>> ((PureThy.add_defs_i false o map Thm.no_attributes)
+      |> ((PureThy.add_defs false o map Thm.no_attributes) sel_specs)
+      ||>> ((PureThy.add_defs false o map Thm.no_attributes) upd_specs)
+      ||>> ((PureThy.add_defs false o map Thm.no_attributes)
              [make_spec, fields_spec, extend_spec, truncate_spec])
       |-> (fn defs as ((sel_defs, upd_defs), derived_defs) =>
           fold Code.add_default_func sel_defs
diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Tools/specification_package.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -29,7 +29,7 @@
                                else thname
                 val def_eq = Logic.mk_equals (Const(cname_full,ctype),
                                               HOLogic.choice_const ctype $  P)
-                val (thms, thy') = PureThy.add_defs_i covld [((cdefname,def_eq),[])] thy
+                val (thms, thy') = PureThy.add_defs covld [((cdefname,def_eq),[])] thy
                 val thm' = [thm,hd thms] MRS @{thm exE_some}
             in
                 mk_definitional cos (thy',thm')
@@ -40,7 +40,7 @@
         let
             fun process [] (thy,tm) =
                 let
-                    val (thms, thy') = PureThy.add_axioms_i [((axname,HOLogic.mk_Trueprop tm),[])] thy
+                    val (thms, thy') = PureThy.add_axioms [((axname,HOLogic.mk_Trueprop tm),[])] thy
                 in
                     (thy',hd thms)
                 end
diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -128,7 +128,7 @@
     fun add_def eq thy =
       if def then
         thy
-        |> PureThy.add_defs_i false [Thm.no_attributes eq]
+        |> PureThy.add_defs false [Thm.no_attributes eq]
         |-> (fn [th] => pair (SOME th))
       else (NONE, thy);
 
@@ -140,7 +140,7 @@
         [(Rep_name, newT --> oldT, NoSyn),
          (Abs_name, oldT --> newT, NoSyn)])
       #> add_def (PrimitiveDefs.mk_defpair (setC, set))
-      ##>> PureThy.add_axioms_i [((typedef_name, typedef_prop),
+      ##>> PureThy.add_axioms [((typedef_name, typedef_prop),
           [apsnd (fn cond_axm => nonempty RS cond_axm)])]
       ##> Theory.add_deps "" (dest_Const RepC) typedef_deps
       ##> Theory.add_deps "" (dest_Const AbsC) typedef_deps
diff -r 24738db98d34 -r ce171cbd4b93 src/HOLCF/IOA/meta_theory/ioa_package.ML
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -350,7 +350,7 @@
 (automaton_name ^ "_trans",
  "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
 (automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
-|> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
+|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
 [(automaton_name ^ "_initial_def",
 automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
 (automaton_name ^ "_asig_def",
@@ -391,7 +391,7 @@
   Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
    Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
 ,NoSyn)]
-|> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
+|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
 [(automaton_name ^ "_def",
 automaton_name ^ " == " ^ comp_list)]
 end)
@@ -406,7 +406,7 @@
 thy
 |> ContConsts.add_consts_i
 [(automaton_name, auttyp,NoSyn)]
-|> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
+|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
 [(automaton_name ^ "_def",
 automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] 
 end)
@@ -420,7 +420,7 @@
 thy
 |> ContConsts.add_consts_i
 [(automaton_name, auttyp,NoSyn)]
-|> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
+|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
 [(automaton_name ^ "_def",
 automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] 
 end)
@@ -446,7 +446,7 @@
   Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
    Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
 ,NoSyn)]
-|> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
+|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
 [(automaton_name ^ "_def",
 automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
 end)
diff -r 24738db98d34 -r ce171cbd4b93 src/HOLCF/Tools/domain/domain_axioms.ML
--- a/src/HOLCF/Tools/domain/domain_axioms.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -111,10 +111,10 @@
 
 fun infer_props thy = map (apsnd (FixrecPackage.legacy_infer_prop thy));
 
-fun add_axioms_i x = snd o PureThy.add_axioms_i (map Thm.no_attributes x);
+fun add_axioms_i x = snd o PureThy.add_axioms (map Thm.no_attributes x);
 fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy;
 
-fun add_defs_i x = snd o (PureThy.add_defs_i false) (map Thm.no_attributes x);
+fun add_defs_i x = snd o (PureThy.add_defs false) (map Thm.no_attributes x);
 fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
 
 in (* local *)
diff -r 24738db98d34 -r ce171cbd4b93 src/HOLCF/Tools/fixrec_package.ML
--- a/src/HOLCF/Tools/fixrec_package.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOLCF/Tools/fixrec_package.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -97,7 +97,7 @@
     
     val fixdefs = map (apsnd (legacy_infer_prop thy)) pre_fixdefs;
     val (fixdef_thms, thy') =
-      PureThy.add_defs_i false (map Thm.no_attributes fixdefs) thy;
+      PureThy.add_defs false (map Thm.no_attributes fixdefs) thy;
     val ctuple_fixdef_thm = foldr1 (fn (x,y) => @{thm cpair_equalI} OF [x,y]) fixdef_thms;
     
     val ctuple_unfold = legacy_infer_term thy' (mk_trp (mk_ctuple lhss === mk_ctuple rhss));
diff -r 24738db98d34 -r ce171cbd4b93 src/HOLCF/Tools/pcpodef_package.ML
--- a/src/HOLCF/Tools/pcpodef_package.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOLCF/Tools/pcpodef_package.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -90,7 +90,7 @@
       |> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac
       ||> AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.sq_ord"])
            (Class.intro_classes_tac [])
-      ||>> PureThy.add_defs_i true [Thm.no_attributes less_def]
+      ||>> PureThy.add_defs true [Thm.no_attributes less_def]
       |-> (fn ((_, {type_definition, set_def, ...}), [less_definition]) =>
           AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.po"])
              (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1)
diff -r 24738db98d34 -r ce171cbd4b93 src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/Pure/Isar/constdefs.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -50,7 +50,7 @@
     val thy' =
       thy
       |> Sign.add_consts_i [(c, T, mx)]
-      |> PureThy.add_defs_i false [((name, def), atts)]
+      |> PureThy.add_defs false [((name, def), atts)]
       |-> (fn [thm] => Code.add_default_func thm);
   in ((c, T), thy') end;
 
diff -r 24738db98d34 -r ce171cbd4b93 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -192,20 +192,20 @@
 fun add_axms f args thy =
   f (map (fn (x, srcs) => (x, map (Attrib.attribute thy) srcs)) args) thy;
 
-val add_axioms = add_axms (snd oo PureThy.add_axioms);
+val add_axioms = add_axms (snd oo PureThy.add_axioms_cmd);
 
 fun add_defs ((unchecked, overloaded), args) =
   add_axms
-    (snd oo (if unchecked then PureThy.add_defs_unchecked else PureThy.add_defs) overloaded) args;
+    (snd oo (if unchecked then PureThy.add_defs_unchecked_cmd else PureThy.add_defs_cmd) overloaded) args;
 
 
 (* facts *)
 
 fun apply_theorems args thy =
   let val facts = Attrib.map_facts (Attrib.attribute thy) [(("", []), args)]
-  in apfst (maps snd) (PureThy.note_thmss "" facts thy) end;
+  in apfst (maps snd) (PureThy.note_thmss_cmd "" facts thy) end;
 
-fun apply_theorems_i args = apfst (maps snd) o PureThy.note_thmss_i "" [(("", []), args)];
+fun apply_theorems_i args = apfst (maps snd) o PureThy.note_thmss "" [(("", []), args)];
 
 
 (* declarations *)
diff -r 24738db98d34 -r ce171cbd4b93 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -729,7 +729,7 @@
              val (def_thms, thy') = if t = nullt then ([], thy) else
                thy
                |> Sign.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)]
-               |> PureThy.add_defs_i false [((extr_name s vs ^ "_def",
+               |> PureThy.add_defs false [((extr_name s vs ^ "_def",
                     Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
            in
              thy'
diff -r 24738db98d34 -r ce171cbd4b93 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/Pure/axclass.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -468,7 +468,7 @@
     val ([def], def_thy) =
       thy
       |> Sign.primitive_class (bclass, super)
-      |> PureThy.add_defs_i false [((Thm.def_name bconst, class_eq), [])];
+      |> PureThy.add_defs false [((Thm.def_name bconst, class_eq), [])];
     val (raw_intro, (raw_classrel, raw_axioms)) =
       split_defined (length conjs) def ||> chop (length super);
 
@@ -478,10 +478,13 @@
     val class_triv = Thm.class_triv def_thy class;
     val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) =
       def_thy
-      |> PureThy.note_thmss_qualified "" bconst
+      |> Sign.add_path bconst
+      |> Sign.no_base_names
+      |> PureThy.note_thmss ""
         [((introN, []), [([Drule.standard raw_intro], [])]),
          ((superN, []), [(map Drule.standard raw_classrel, [])]),
-         ((axiomsN, []), [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])];
+         ((axiomsN, []), [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]
+      ||> Sign.restore_naming def_thy;
 
 
     (* result *)
@@ -491,7 +494,7 @@
       facts_thy
       |> fold put_classrel (map (pair class) super ~~ classrel)
       |> Sign.add_path bconst
-      |> PureThy.note_thmss_i "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd
+      |> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd
       |> Sign.restore_naming facts_thy
       |> map_axclasses (fn (axclasses, parameters) =>
         (Symtab.update (class, axclass) axclasses,
@@ -510,7 +513,7 @@
     val args = prep thy raw_args;
     val specs = mk args;
     val names = name args;
-  in thy |> PureThy.add_axioms_i (map (rpair []) (names ~~ specs)) |-> fold add end;
+  in thy |> PureThy.add_axioms (map (rpair []) (names ~~ specs)) |-> fold add end;
 
 fun ax_classrel prep =
   axiomatize (map o prep) (map Logic.mk_classrel)
diff -r 24738db98d34 -r ce171cbd4b93 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/Pure/pure_thy.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -43,27 +43,25 @@
   val store_thms: bstring * thm list -> theory -> thm list * theory
   val store_thm: bstring * thm -> theory -> thm * theory
   val store_thm_open: bstring * thm -> theory -> thm * theory
+  val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory
   val add_thm: (bstring * thm) * attribute list -> theory -> thm * theory
-  val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory
   val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory
   val add_thms_dynamic: bstring * (Context.generic -> thm list) -> theory -> theory
   val note_thmss: string -> ((bstring * attribute list) *
-    (Facts.ref * attribute list) list) list -> theory -> (bstring * thm list) list * theory
-  val note_thmss_i: string -> ((bstring * attribute list) *
     (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory
   val note_thmss_grouped: string -> string -> ((bstring * attribute list) *
     (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory
-  val note_thmss_qualified: string -> string -> ((bstring * attribute list) *
-    (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory
-  val add_axioms: ((bstring * string) * attribute list) list -> theory -> thm list * theory
-  val add_axioms_i: ((bstring * term) * attribute list) list -> theory -> thm list * theory
-  val add_defs: bool -> ((bstring * string) * attribute list) list ->
+  val note_thmss_cmd: string -> ((bstring * attribute list) *
+    (Facts.ref * attribute list) list) list -> theory -> (bstring * thm list) list * theory
+  val add_axioms: ((bstring * term) * attribute list) list -> theory -> thm list * theory
+  val add_axioms_cmd: ((bstring * string) * attribute list) list -> theory -> thm list * theory
+  val add_defs: bool -> ((bstring * term) * attribute list) list ->
     theory -> thm list * theory
-  val add_defs_i: bool -> ((bstring * term) * attribute list) list ->
+  val add_defs_unchecked: bool -> ((bstring * term) * attribute list) list ->
     theory -> thm list * theory
-  val add_defs_unchecked: bool -> ((bstring * string) * attribute list) list ->
+  val add_defs_unchecked_cmd: bool -> ((bstring * string) * attribute list) list ->
     theory -> thm list * theory
-  val add_defs_unchecked_i: bool -> ((bstring * term) * attribute list) list ->
+  val add_defs_cmd: bool -> ((bstring * string) * attribute list) list ->
     theory -> thm list * theory
   val old_appl_syntax: theory -> bool
   val old_appl_syntax_setup: theory -> theory
@@ -252,19 +250,12 @@
 
 in
 
-fun note_thmss k = gen_note_thmss (fn thy => get_fact (Context.Theory thy) thy) (kind k);
-fun note_thmss_i k = gen_note_thmss (K I) (kind k);
+fun note_thmss k = gen_note_thmss (K I) (kind k);
 fun note_thmss_grouped k g = gen_note_thmss (K I) (kind k #> group g);
+fun note_thmss_cmd k = gen_note_thmss (fn thy => get_fact (Context.Theory thy) thy) (kind k);
 
 end;
 
-fun note_thmss_qualified k path facts thy =
-  thy
-  |> Sign.add_path path
-  |> Sign.no_base_names
-  |> note_thmss_i k facts
-  ||> Sign.restore_naming thy;
-
 
 (* store axioms as theorems *)
 
@@ -278,12 +269,12 @@
       val thm = hd (get_axs thy' named_ax);
     in apfst hd (gen_add_thms (K I) [((name, thm), atts)] thy') end);
 in
-  val add_axioms           = add_axm Theory.add_axioms;
-  val add_axioms_i         = add_axm Theory.add_axioms_i;
-  val add_defs             = add_axm o Theory.add_defs false;
-  val add_defs_i           = add_axm o Theory.add_defs_i false;
-  val add_defs_unchecked   = add_axm o Theory.add_defs true;
-  val add_defs_unchecked_i = add_axm o Theory.add_defs_i true;
+  val add_defs               = add_axm o Theory.add_defs_i false;
+  val add_defs_unchecked     = add_axm o Theory.add_defs_i true;
+  val add_axioms             = add_axm Theory.add_axioms_i;
+  val add_defs_cmd           = add_axm o Theory.add_defs false;
+  val add_defs_unchecked_cmd = add_axm o Theory.add_defs true;
+  val add_axioms_cmd         = add_axm Theory.add_axioms;
 end;
 
 
@@ -414,7 +405,7 @@
   #> Sign.add_consts_i
    [("term", typ "'a => prop", NoSyn),
     ("conjunction", typ "prop => prop => prop", NoSyn)]
-  #> (add_defs_i false o map Thm.no_attributes)
+  #> (add_defs false o map Thm.no_attributes)
    [("prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
     ("term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
     ("conjunction_def", prop "(A && B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
diff -r 24738db98d34 -r ce171cbd4b93 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -247,14 +247,14 @@
       if need_recursor then
            thy |> Sign.add_consts_i
                     [(recursor_base_name, recursor_typ, NoSyn)]
-               |> (snd o PureThy.add_defs_i false [Thm.no_attributes recursor_def])
+               |> (snd o PureThy.add_defs false [Thm.no_attributes recursor_def])
       else thy;
 
   val (con_defs, thy0) = thy_path
              |> Sign.add_consts_i
                  ((case_base_name, case_typ, NoSyn) ::
                   map #1 (List.concat con_ty_lists))
-             |> PureThy.add_defs_i false
+             |> PureThy.add_defs false
                  (map Thm.no_attributes
                   (case_def ::
                    List.concat (ListPair.map mk_con_defs
diff -r 24738db98d34 -r ce171cbd4b93 src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/ZF/Tools/ind_cases.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -52,7 +52,7 @@
     val facts = args |> map (fn ((name, srcs), props) =>
       ((name, map (Attrib.attribute thy) srcs),
         map (Thm.no_attributes o single o mk_cases) props));
-  in thy |> PureThy.note_thmss_i "" facts |> snd end;
+  in thy |> PureThy.note_thmss "" facts |> snd end;
 
 
 (* ind_cases method *)
diff -r 24738db98d34 -r ce171cbd4b93 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -174,7 +174,7 @@
   val (_, thy1) =
     thy
     |> Sign.add_path big_rec_base_name
-    |> PureThy.add_defs_i false (map Thm.no_attributes axpairs);
+    |> PureThy.add_defs false (map Thm.no_attributes axpairs);
 
   val ctxt1 = ProofContext.init thy1;
 
diff -r 24738db98d34 -r ce171cbd4b93 src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/ZF/Tools/primrec_package.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -170,7 +170,7 @@
 
     val ([def_thm], thy1) = thy
       |> Sign.add_path (Sign.base_name fname)
-      |> (PureThy.add_defs_i false o map Thm.no_attributes) [def];
+      |> (PureThy.add_defs false o map Thm.no_attributes) [def];
 
     val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
     val eqn_thms =