axiomatization: declare Spec_Rules, direct result;

--- a/src/Pure/Isar/specification.ML	Sun Nov 15 20:56:34 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Sun Nov 15 20:57:42 2009 +0100
@@ -28,10 +28,10 @@
     (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   val axiomatization: (binding * typ option * mixfix) list ->
     (Attrib.binding * term list) list -> theory ->
-    (term list * (string * thm list) list) * theory
+    (term list * thm list list) * theory
   val axiomatization_cmd: (binding * string option * mixfix) list ->
     (Attrib.binding * string list) list -> theory ->
-    (term list * (string * thm list) list) * theory
+    (term list * thm list list) * theory
   val definition:
     (binding * typ option * mixfix) option * (Attrib.binding * term) ->
     local_theory -> (term * (string * thm)) * local_theory
@@ -169,16 +169,18 @@
         fold_map Thm.add_axiom
           (map (apfst (fn a => Binding.map_name (K a) b))
             (PureThy.name_multi (Name.of_binding b) (map subst props)))
-        #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])])));
+        #>> (fn ths => ((b, atts), [(ths, [])])));
 
     (*facts*)
-    val (facts, thy') = axioms_thy |> PureThy.note_thmss ""
-      (Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);
+    val (facts, facts_lthy) = axioms_thy
+      |> Theory_Target.init NONE
+      |> Spec_Rules.add Spec_Rules.Unknown (consts, maps (maps #1 o #2) axioms)
+      |> Local_Theory.notes axioms;
 
     val _ =
       if not do_print then ()
-      else print_consts (ProofContext.init thy') (K false) xs;
-  in ((consts, facts), thy') end;
+      else print_consts facts_lthy (K false) xs;
+  in ((consts, map #2 facts), Local_Theory.exit_global facts_lthy) end;
 
 val axiomatization = gen_axioms false check_specification;
 val axiomatization_cmd = gen_axioms true read_specification;