pattern_matches: add to bossLib

HOL-Theorem-Prover · Dec 25, 2015 · b67a219 · b67a219
1 parent 910f1a9
commit b67a219
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git a/src/boss/bossLib.sml b/src/boss/bossLib.sml
@@ -15,7 +15,7 @@ structure bossLib :> bossLib =
 struct
 
 open HolKernel Parse boolLib pairLib simpLib metisLib pred_setLib
-     boolSimps quantHeuristicsLib
+     boolSimps quantHeuristicsLib patternMatchesLib
 
 (* This makes the dependency on listTheory and optionTheory explicit.
    Without it, the theories can change, and bossLib won't get recompiled.
@@ -102,9 +102,9 @@ in
 val QI_ss = quantHeuristicsLib.QUANT_INST_ss [std_qp]
 val pure_ss = pureSimps.pure_ss
 val bool_ss = boolSimps.bool_ss
-val std_ss = numLib.std_ss
-val arith_ss = numLib.arith_ss
-val old_arith_ss = std_ss ++ numSimps.old_ARITH_ss
+val std_ss = numLib.std_ss ++ PMATCH_SIMP_ss
+val arith_ss = numLib.arith_ss ++ PMATCH_SIMP_ss
+val old_arith_ss = std_ss ++ numSimps.old_ARITH_ss ++ PMATCH_SIMP_ss
 val ARITH_ss = numSimps.ARITH_ss
 val old_ARITH_ss = numSimps.old_ARITH_ss
 val list_ss  = arith_ss ++ listSimps.LIST_ss

diff --git a/src/pattern_matches/patternMatchesLib.sml b/src/pattern_matches/patternMatchesLib.sml
@@ -1490,7 +1490,7 @@ val PMATCH_SIMP_CONV = PMATCH_SIMP_CONV_GEN [];
 fun PMATCH_SIMP_GEN_ss ssl =
   make_gen_conv_ss PMATCH_SIMP_CONV_GENCALL "PMATCH_SIMP_REDUCER" ssl
 
-val PMATCH_SIMP_ss = PMATCH_SIMP_GEN_ss []
+val PMATCH_SIMP_ss = name_ss "patternMatchesSimp" (PMATCH_SIMP_GEN_ss [])
 
 
 (***********************************************)