Facts.dest/export_static: content difference;
authorwenzelm
Thu Jun 12 16:41:47 2008 +0200 (2008-06-12)
changeset 271739ae98c3cd3d6
parent 27172 8236f13be95b
child 27174 c2c484480f40
Facts.dest/export_static: content difference;
src/HOL/Import/shuffler.ML
src/Pure/Isar/find_theorems.ML
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/HOL/Import/shuffler.ML	Thu Jun 12 15:49:25 2008 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Thu Jun 12 16:41:47 2008 +0200
     1.3 @@ -624,7 +624,7 @@
     1.4          val shuffles = ShuffleData.get thy
     1.5          val ignored = collect_ignored shuffles []
     1.6          val all_thms =
     1.7 -          map (`PureThy.get_name_hint) (maps #2 (Facts.dest_static (PureThy.facts_of thy)))
     1.8 +          map (`PureThy.get_name_hint) (maps #2 (Facts.dest_static [] (PureThy.facts_of thy)))
     1.9      in
    1.10          List.filter (match_consts ignored t) all_thms
    1.11      end
     2.1 --- a/src/Pure/Isar/find_theorems.ML	Thu Jun 12 15:49:25 2008 +0200
     2.2 +++ b/src/Pure/Isar/find_theorems.ML	Thu Jun 12 16:41:47 2008 +0200
     2.3 @@ -273,8 +273,8 @@
     2.4  
     2.5  fun all_facts_of ctxt =
     2.6    maps Facts.selections
     2.7 -   (Facts.dest_static (PureThy.facts_of (ProofContext.theory_of ctxt)) @
     2.8 -    Facts.dest_static (ProofContext.facts_of ctxt));
     2.9 +   (Facts.dest_static [] (PureThy.facts_of (ProofContext.theory_of ctxt)) @
    2.10 +    Facts.dest_static [] (ProofContext.facts_of ctxt));
    2.11  
    2.12  val limit = ref 40;
    2.13  
     3.1 --- a/src/Pure/Isar/proof_context.ML	Thu Jun 12 15:49:25 2008 +0200
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Jun 12 16:41:47 2008 +0200
     3.3 @@ -1184,7 +1184,8 @@
     3.4      val local_facts = facts_of ctxt;
     3.5      val props = Facts.props local_facts;
     3.6      val facts =
     3.7 -      (if null props then [] else [("unnamed", props)]) @ Facts.extern_static local_facts;
     3.8 +      (if null props then [] else [("unnamed", props)]) @
     3.9 +      Facts.extern_static [] local_facts;
    3.10    in
    3.11      if null facts andalso not (! verbose) then []
    3.12      else [Pretty.big_list "facts:" (map (pretty_fact ctxt) facts)]