# HG changeset patch
# User wenzelm
# Date 1164769875 -3600
# Node ID ac6af184bfb08d95794c79e0df5e8bdb1d8d6370
# Parent  7799b1739a51417c17df2207a7bbe57b860b9934
simplified add_thmss;
mark predicate definitions as internal;

diff -r 7799b1739a51 -r ac6af184bfb0 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Nov 29 04:11:14 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Wed Nov 29 04:11:15 2006 +0100
@@ -92,7 +92,7 @@
   (* Storing results *)
   val add_thmss: string -> string ->
     ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
-    Proof.context -> (string * thm list) list * Proof.context
+    Proof.context -> Proof.context
   val add_type_syntax: string -> (morphism -> Proof.context -> Proof.context) ->
     Proof.context -> Proof.context
   val add_term_syntax: string -> (morphism -> Proof.context -> Proof.context) ->
@@ -1571,7 +1571,7 @@
 
 fun add_thmss loc kind args ctxt =
   let
-    val (ctxt', ([(_, [Notes args'])], facts)) =
+    val (ctxt', ([(_, [Notes args'])], _)) =
       activate_facts true cert_facts
         (ctxt, [((("", []), Assumed []), [Ext (Notes (kind, args))])]);
     val ctxt'' = ctxt' |> ProofContext.theory
@@ -1580,7 +1580,7 @@
           (axiom, import, elems @ [(Notes args', stamp ())],
             params, lparams, decls, regs, intros))
       #> note_thmss_registrations loc args');
-  in (facts, ctxt'') end;
+  in ctxt'' end;
 
 
 
@@ -1709,7 +1709,7 @@
             thy |> def_pred aname parms defs exts exts';
           val elemss' = change_assumes_elemss axioms elemss;
           val def_thy' = def_thy
-            |> PureThy.note_thmss_qualified Thm.definitionK
+            |> PureThy.note_thmss_qualified Thm.internalK
               aname [((introN, []), [([intro], [])])]
             |> snd;
           val a_elem = [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
@@ -1724,7 +1724,7 @@
           val elemss'' = change_elemss_hyps axioms elemss';
           val def_thy' =
           def_thy
-          |> PureThy.note_thmss_qualified Thm.definitionK bname
+          |> PureThy.note_thmss_qualified Thm.internalK bname
               [((introN, []), [([intro], [])]),
                 ((axiomsN, []), [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
           |> snd;