File tree Expand file tree Collapse file tree 3 files changed +3
-3
lines changed Expand file tree Collapse file tree 3 files changed +3
-3
lines changed Original file line number Diff line number Diff line change @@ -18,7 +18,7 @@ open HolKernel Parse basicHol90Lib;
18
18
type thm = Thm.thm;
19
19
20
20
val ambient_grammars = Parse.current_grammars();
21
- val _ = Parse.temp_set_grammars boolTheory.bool_grammars
21
+ val _ = Parse.temp_set_grammars $ valOf $ grammarDB {thyname= " bool " }
22
22
23
23
fun decompose (tm, args_so_far) =
24
24
if is_comb tm then
Original file line number Diff line number Diff line change @@ -83,7 +83,7 @@ type thm = Thm.thm;
83
83
84
84
85
85
val ambient_grammars = Parse.current_grammars();
86
- val _ = Parse.temp_set_grammars boolTheory.bool_grammars
86
+ val _ = Parse.temp_set_grammars $ valOf $ grammarDB {thyname= " bool " }
87
87
88
88
89
89
(* define_mutual_functions takes the term def (one such as the one above)
Original file line number Diff line number Diff line change @@ -7,7 +7,7 @@ open state_transformerTheory
7
7
structure Parse = struct
8
8
open Parse
9
9
val (Type, Term) =
10
- parse_from_grammars state_transformerTheory.state_transformer_grammars
10
+ parse_from_grammars $ valOf $ grammarDB {thyname= " state_transformer " }
11
11
end
12
12
open Parse
13
13
You can’t perform that action at this time.
0 commit comments