equal
deleted
inserted
replaced
17 end; |
17 end; |
18 |
18 |
19 structure Reconstruct : RECONSTRUCT = |
19 structure Reconstruct : RECONSTRUCT = |
20 struct |
20 struct |
21 |
21 |
22 val quiet_mode = |
22 val quiet_mode = Config.declare_bool ("Reconstruct.quiet_mode", \<^here>) (K true); |
23 Config.bool (Config.declare ("Reconstruct.quiet_mode", \<^here>) (K (Config.Bool true))); |
|
24 |
23 |
25 fun message ctxt msg = |
24 fun message ctxt msg = |
26 if Config.get ctxt quiet_mode then () else writeln (msg ()); |
25 if Config.get ctxt quiet_mode then () else writeln (msg ()); |
27 |
26 |
28 fun vars_of t = map Var (rev (Term.add_vars t [])); |
27 fun vars_of t = map Var (rev (Term.add_vars t [])); |