# HG changeset patch
# User boehmes
# Date 1281234531 -7200
# Node ID 27da291ee2021bf4a1586300fa47c59efe7db764
# Parent  59484a20c48ff6ba700e4b396db2095f23f992ad
added scanning of if-then-else expressions

diff -r 59484a20c48f -r 27da291ee202 src/HOL/Boogie/Tools/boogie_loader.ML
--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Aug 06 18:14:18 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Sun Aug 08 04:28:51 2010 +0200
@@ -341,7 +341,7 @@
   in
     (case Scan.error (Scan.finite (stopper i) scan) ts of
       (x, []) => x
-    | (_, ts) => error (scan_err "unparsed input" ts))
+    | (_, ts') => error (scan_err "unparsed input" ts'))
   end
 
 fun read_int' s = (case read_int (explode s) of (i, []) => SOME i | _ => NONE)
@@ -499,6 +499,11 @@
         mk_nary (curry HOLogic.mk_conj) @{term True} ||
       scan_line "or" num :|-- scan_count exp >>
         mk_nary (curry HOLogic.mk_disj) @{term False} ||
+      scan_line' "ite" |-- exp -- exp -- exp >> (fn ((c, t1), t2) =>
+        let val T = Term.fastype_of t1
+        in
+          Const (@{const_name If}, [@{typ bool}, T, T] ---> T) $ c $ t1 $ t2
+        end) ||
       binexp "implies" (binop @{term "op -->"}) ||
       scan_line "distinct" num :|-- scan_count exp >>
         (fn [] => @{term True}