Facts.dest_table;
authorwenzelm
Tue Apr 15 18:49:15 2008 +0200 (2008-04-15)
changeset 2666239483503705f
parent 26661 53e541e5b432
child 26663 020618551468
Facts.dest_table;
src/HOL/Import/shuffler.ML
src/HOL/Tools/res_atp.ML
src/Tools/code/code_package.ML
     1.1 --- a/src/HOL/Import/shuffler.ML	Tue Apr 15 18:49:13 2008 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Tue Apr 15 18:49:15 2008 +0200
     1.3 @@ -623,7 +623,8 @@
     1.4      let
     1.5          val shuffles = ShuffleData.get thy
     1.6          val ignored = collect_ignored shuffles []
     1.7 -        val all_thms = map (`PureThy.get_name_hint) (maps #2 (Facts.dest (PureThy.all_facts_of thy)))
     1.8 +        val all_thms =
     1.9 +          map (`PureThy.get_name_hint) (maps #2 (Facts.dest_table (PureThy.facts_of thy)))
    1.10      in
    1.11          List.filter (match_consts ignored t) all_thms
    1.12      end
     2.1 --- a/src/HOL/Tools/res_atp.ML	Tue Apr 15 18:49:13 2008 +0200
     2.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Apr 15 18:49:15 2008 +0200
     2.3 @@ -480,7 +480,7 @@
     2.4      fun dest_valid (space, tab) = Symtab.fold (extern_valid space) tab [];
     2.5    in
     2.6      maps (dest_valid o PureThy.theorems_of) all_thys @
     2.7 -    fold (extern_valid (Facts.space_of local_facts)) (Facts.dest local_facts) []
     2.8 +    fold (extern_valid (Facts.space_of local_facts)) (Facts.dest_table local_facts) []
     2.9    end;
    2.10  
    2.11  fun multi_name a (th, (n,pairs)) =
     3.1 --- a/src/Tools/code/code_package.ML	Tue Apr 15 18:49:13 2008 +0200
     3.2 +++ b/src/Tools/code/code_package.ML	Tue Apr 15 18:49:15 2008 +0200
     3.3 @@ -223,7 +223,7 @@
     3.4          val propdef = (((c, ty), tfree_vars @ map Free vars), t);
     3.5        in if c = "" then NONE else SOME (thmref, propdef) end;
     3.6    in
     3.7 -    Facts.dest (PureThy.all_facts_of thy)
     3.8 +    Facts.dest_table (PureThy.facts_of thy)
     3.9      |> maps Facts.selections
    3.10      |> map_filter select
    3.11      |> map_filter mk_codeprop