--- a/src/HOL/SMT_Examples/boogie.ML Mon Sep 24 14:30:09 2018 +0200
+++ b/src/HOL/SMT_Examples/boogie.ML Mon Sep 24 16:09:27 2018 +0200
@@ -139,7 +139,7 @@
parse_bin_expr cx (mk_binary @{term "(<=) :: int => _"} o swap) ls
| parse_expr cx (["+"] :: ls) = parse_bin_expr cx (mk_binary @{term "(+) :: int => _"}) ls
| parse_expr cx (["-"] :: ls) = parse_bin_expr cx (mk_binary @{term "(-) :: int => _"}) ls
- | parse_expr cx (["*"] :: ls) = parse_bin_expr cx (mk_binary @{term "( * ) :: int => _"}) ls
+ | parse_expr cx (["*"] :: ls) = parse_bin_expr cx (mk_binary @{term "(*) :: int => _"}) ls
| parse_expr cx (["/"] :: ls) = parse_bin_expr cx (mk_binary @{term boogie_div}) ls
| parse_expr cx (["%"] :: ls) = parse_bin_expr cx (mk_binary @{term boogie_mod}) ls
| parse_expr cx (["select", n] :: ls) =