# HG changeset patch
# User wenzelm
# Date 1213281707 -7200
# Node ID 9ae98c3cd3d63468143ba5d9ded316df36a1c1bf
# Parent  8236f13be95b42fd2b04421178be84b2517e8b74
Facts.dest/export_static: content difference;

diff -r 8236f13be95b -r 9ae98c3cd3d6 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Thu Jun 12 15:49:25 2008 +0200
+++ b/src/HOL/Import/shuffler.ML	Thu Jun 12 16:41:47 2008 +0200
@@ -624,7 +624,7 @@
         val shuffles = ShuffleData.get thy
         val ignored = collect_ignored shuffles []
         val all_thms =
-          map (`PureThy.get_name_hint) (maps #2 (Facts.dest_static (PureThy.facts_of thy)))
+          map (`PureThy.get_name_hint) (maps #2 (Facts.dest_static [] (PureThy.facts_of thy)))
     in
         List.filter (match_consts ignored t) all_thms
     end
diff -r 8236f13be95b -r 9ae98c3cd3d6 src/Pure/Isar/find_theorems.ML
--- a/src/Pure/Isar/find_theorems.ML	Thu Jun 12 15:49:25 2008 +0200
+++ b/src/Pure/Isar/find_theorems.ML	Thu Jun 12 16:41:47 2008 +0200
@@ -273,8 +273,8 @@
 
 fun all_facts_of ctxt =
   maps Facts.selections
-   (Facts.dest_static (PureThy.facts_of (ProofContext.theory_of ctxt)) @
-    Facts.dest_static (ProofContext.facts_of ctxt));
+   (Facts.dest_static [] (PureThy.facts_of (ProofContext.theory_of ctxt)) @
+    Facts.dest_static [] (ProofContext.facts_of ctxt));
 
 val limit = ref 40;
 
diff -r 8236f13be95b -r 9ae98c3cd3d6 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Jun 12 15:49:25 2008 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Jun 12 16:41:47 2008 +0200
@@ -1184,7 +1184,8 @@
     val local_facts = facts_of ctxt;
     val props = Facts.props local_facts;
     val facts =
-      (if null props then [] else [("unnamed", props)]) @ Facts.extern_static local_facts;
+      (if null props then [] else [("unnamed", props)]) @
+      Facts.extern_static [] local_facts;
   in
     if null facts andalso not (! verbose) then []
     else [Pretty.big_list "facts:" (map (pretty_fact ctxt) facts)]