Revert "make patricia play nice..."

This reverts commit da47401. Reason: qualified names in the list of add_persistent_funs exports are supposed to work. See comments on #73. The reason why they probably weren't working before is that you need to use a name like: "pred_set.FINITE_EMPTY" not "pred_setTheory.FINITE_EMPTY" Conflicts: src/list/src/listScript.sml src/patricia/patriciaScript.sml src/patricia/patricia_castsScript.sml src/pred_set/src/pred_setScript.sml (Conflicts all due to change in add_persistent_funs interface.)
HOL-Theorem-Prover · Jul 31, 2012 · fa6472b · fa6472b
1 parent ccba08b
commit fa6472b
Show file tree

Hide file tree

Showing 4 changed files with 15 additions and 21 deletions.
diff --git a/src/list/src/listScript.sml b/src/list/src/listScript.sml
@@ -2681,7 +2681,4 @@ fun dest_list M =
                else raise ERR "dest_list" "not terminated with nil"
      | SOME(h,t) => h::dest_list t
 
-val _ = computeLib.add_persistent_funs ["LIST_TO_SET_THM"]
-
 val _ = export_theory();
-
diff --git a/src/patricia/patriciaScript.sml b/src/patricia/patriciaScript.sml
@@ -1040,10 +1040,17 @@ val DELETE_UNION = store_thm("DELETE_UNION",
   SRW_TAC [] [pred_setTheory.EXTENSION] \\ METIS_TAC []);
 
 val _ = computeLib.add_persistent_funs
-  ["DELETE_UNION"
-  ,"TRAVERSE_AUX"
-  ,"ADD_INSERT"
-  ,"PTREE_OF_NUMSET_EMPTY"];
+  ["list.LIST_TO_SET_THM",
+   "pred_set.EMPTY_DELETE",
+   "pred_set.DELETE_INSERT",
+   "DELETE_UNION",
+   "pred_set.FINITE_EMPTY",
+   "pred_set.FINITE_INSERT",
+   "pred_set.FINITE_UNION",
+   "pred_set.FINITE_DELETE",
+   "TRAVERSE_AUX",
+   "ADD_INSERT",
+   "PTREE_OF_NUMSET_EMPTY"];
 
 (* ------------------------------------------------------------------------- *)
 

diff --git a/src/patricia/patricia_castsScript.sml b/src/patricia/patricia_castsScript.sml
@@ -380,7 +380,10 @@ val _ = add_listform {leftdelim = [TOK "-{"], rightdelim = [TOK "}-"],
                       block_info = (PP.INCONSISTENT, 0)};
 
 val _ = computeLib.add_persistent_funs
-  ["ADD_INSERT_WORD",
+  ["pred_set.IMAGE_EMPTY",
+   "pred_set.IMAGE_INSERT",
+   "pred_set.IMAGE_UNION",
+   "ADD_INSERT_WORD",
    "ADD_INSERT_STRING",
    "THE_PTREE_SOME_PTREE"];
 

diff --git a/src/pred_set/src/pred_setScript.sml b/src/pred_set/src/pred_setScript.sml
@@ -5016,17 +5016,4 @@ val _ = adjoin_to_theory
       "     encode=NONE})];\n"
       ] end)};
 
-val _ = computeLib.add_persistent_funs
-  ["EMPTY_DELETE"
-  ,"DELETE_INSERT"
-  ,"FINITE_EMPTY"
-  ,"FINITE_INSERT"
-  ,"FINITE_UNION"
-  ,"FINITE_DELETE"
-  ,"IMAGE_EMPTY"
-  ,"IMAGE_INSERT"
-  ,"IMAGE_UNION"]
-
 val _ = export_theory();
-
-