1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Apr 18 10:53:28 2012 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Apr 18 10:53:28 2012 +0200
     1.3 @@ -350,8 +350,13 @@
     1.4  
     1.5    fun as_term t = @{const HOL.eq (bool)} $ t $ @{const SMT.term_true}
     1.6  
     1.7 -  fun wrap_in_if t =
     1.8 -    @{const If (bool)} $ t $ @{const SMT.term_true} $ @{const SMT.term_false}
     1.9 +  exception BAD_PATTERN of unit
    1.10 +
    1.11 +  fun wrap_in_if pat t =
    1.12 +    if pat then
    1.13 +      raise BAD_PATTERN ()
    1.14 +    else
    1.15 +      @{const If (bool)} $ t $ @{const SMT.term_true} $ @{const SMT.term_false}
    1.16  
    1.17    fun is_builtin_conn_or_pred ctxt c ts =
    1.18      is_some (SMT_Builtin.dest_builtin_conn ctxt c ts) orelse
    1.19 @@ -368,30 +373,34 @@
    1.20  
    1.21  fun folify ctxt =
    1.22    let
    1.23 -    fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
    1.24 +    fun in_list T f t = HOLogic.mk_list T (map_filter f (HOLogic.dest_list t))
    1.25  
    1.26 -    fun in_term t =
    1.27 +    fun in_term pat t =
    1.28        (case Term.strip_comb t of
    1.29          (@{const True}, []) => @{const SMT.term_true}
    1.30        | (@{const False}, []) => @{const SMT.term_false}
    1.31        | (u as Const (@{const_name If}, _), [t1, t2, t3]) =>
    1.32 -          u $ in_form t1 $ in_term t2 $ in_term t3
    1.33 +          if pat then raise BAD_PATTERN ()
    1.34 +          else u $ in_form t1 $ in_term pat t2 $ in_term pat t3
    1.35        | (Const (c as (n, _)), ts) =>
    1.36 -          if is_builtin_conn_or_pred ctxt c ts then wrap_in_if (in_form t)
    1.37 -          else  if is_quant n then wrap_in_if (in_form t)
    1.38 -          else Term.list_comb (Const c, map in_term ts)
    1.39 -      | (Free c, ts) => Term.list_comb (Free c, map in_term ts)
    1.40 +          if is_builtin_conn_or_pred ctxt c ts then wrap_in_if pat (in_form t)
    1.41 +          else if is_quant n then wrap_in_if pat (in_form t)
    1.42 +          else Term.list_comb (Const c, map (in_term pat) ts)
    1.43 +      | (Free c, ts) => Term.list_comb (Free c, map (in_term pat) ts)
    1.44        | _ => t)
    1.45  
    1.46      and in_weight ((c as @{const SMT.weight}) $ w $ t) = c $ w $ in_form t
    1.47        | in_weight t = in_form t 
    1.48  
    1.49 -    and in_pat ((p as Const (@{const_name SMT.pat}, _)) $ t) = p $ in_term t
    1.50 -      | in_pat ((p as Const (@{const_name SMT.nopat}, _)) $ t) = p $ in_term t
    1.51 +    and in_pat ((p as Const (@{const_name SMT.pat}, _)) $ t) =
    1.52 +          p $ in_term true t
    1.53 +      | in_pat ((p as Const (@{const_name SMT.nopat}, _)) $ t) =
    1.54 +          p $ in_term true t
    1.55        | in_pat t = raise TERM ("bad pattern", [t])
    1.56  
    1.57      and in_pats ps =
    1.58 -      in_list @{typ "SMT.pattern list"} (in_list @{typ SMT.pattern} in_pat) ps
    1.59 +      in_list @{typ "SMT.pattern list"}
    1.60 +        (SOME o in_list @{typ SMT.pattern} (try in_pat)) ps
    1.61  
    1.62      and in_trigger ((c as @{const SMT.trigger}) $ p $ t) =
    1.63            c $ in_pats p $ in_weight t
    1.64 @@ -401,15 +410,15 @@
    1.65        (case Term.strip_comb t of
    1.66          (q as Const (qn, _), [Abs (n, T, u)]) =>
    1.67            if is_quant qn then q $ Abs (n, T, in_trigger u)
    1.68 -          else as_term (in_term t)
    1.69 +          else as_term (in_term false t)
    1.70        | (Const c, ts) =>
    1.71            (case SMT_Builtin.dest_builtin_conn ctxt c ts of
    1.72              SOME (_, _, us, mk) => mk (map in_form us)
    1.73            | NONE =>
    1.74                (case SMT_Builtin.dest_builtin_pred ctxt c ts of
    1.75 -                SOME (_, _, us, mk) => mk (map in_term us)
    1.76 -              | NONE => as_term (in_term t)))
    1.77 -      | _ => as_term (in_term t))
    1.78 +                SOME (_, _, us, mk) => mk (map (in_term false) us)
    1.79 +              | NONE => as_term (in_term false t)))
    1.80 +      | _ => as_term (in_term false t))
    1.81    in
    1.82      map in_form #>
    1.83      cons (SMT_Utils.prop_of term_bool) #>