1.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Thu Aug 26 13:44:50 2010 +0200
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Thu Aug 26 20:51:17 2010 +0200
     1.3 @@ -504,7 +504,7 @@
     1.4          in
     1.5            Const (@{const_name If}, [@{typ bool}, T, T] ---> T) $ c $ t1 $ t2
     1.6          end) ||
     1.7 -      binexp "implies" (binop @{term "op -->"}) ||
     1.8 +      binexp "implies" (binop @{term HOL.implies}) ||
     1.9        scan_line "distinct" num :|-- scan_count exp >>
    1.10          (fn [] => @{term True}
    1.11            | ts as (t :: _) => mk_distinct (Term.fastype_of t) ts) ||