Fix more grammars

ordinarymath · mn200 · commit 48a676cadda7 · 2025-04-11T13:19:32.000+10:00
diff --git a/src/datatype/mutrec/ConsThms.sml b/src/datatype/mutrec/ConsThms.sml
@@ -18,7 +18,7 @@ open HolKernel Parse basicHol90Lib;
 type thm = Thm.thm;
 
 val ambient_grammars = Parse.current_grammars();
-val _ = Parse.temp_set_grammars boolTheory.bool_grammars
+val _ = Parse.temp_set_grammars $ valOf $ grammarDB {thyname="bool"}
 
 fun decompose (tm, args_so_far) =
     if is_comb tm then
diff --git a/src/datatype/mutrec/Recftn.sml b/src/datatype/mutrec/Recftn.sml
@@ -83,7 +83,7 @@ type thm = Thm.thm;
 
 
 val ambient_grammars = Parse.current_grammars();
-val _ = Parse.temp_set_grammars boolTheory.bool_grammars
+val _ = Parse.temp_set_grammars $ valOf $ grammarDB {thyname="bool"}
 
 
 (* define_mutual_functions takes the term def (one such as the one above)
diff --git a/src/monad/more_monads/state_monadLib.sml b/src/monad/more_monads/state_monadLib.sml
@@ -7,7 +7,7 @@ open state_transformerTheory
 structure Parse = struct
   open Parse
   val (Type, Term) =
-    parse_from_grammars state_transformerTheory.state_transformer_grammars
+    parse_from_grammars $ valOf $ grammarDB {thyname="state_transformer"}
 end
 open Parse
 
