--- a/src/HOL/SMT_Examples/boogie.ML Fri Nov 27 19:56:30 2020 +0100
+++ b/src/HOL/SMT_Examples/boogie.ML Fri Nov 27 21:59:23 2020 +0100
@@ -268,10 +268,10 @@
val _ =
Outer_Syntax.command \<^command_keyword>\<open>boogie_file\<close>
"prove verification condition from .b2i file"
- (Resources.provide_parse_files "boogie_file" >> (fn files =>
+ (Resources.provide_parse_file >> (fn get_file =>
Toplevel.theory (fn thy =>
let
- val ([{lines, ...}], thy') = files thy;
+ val ({lines, ...}, thy') = get_file thy;
val _ = boogie_prove thy' lines;
in thy' end)))