src/HOL/Tools/SMT/z3_model.ML
changeset 40579 98ebd2300823
parent 40551 a0dd429e97d9
child 40627 becf5d5187cc
     1.1 --- a/src/HOL/Tools/SMT/z3_model.ML	Wed Nov 17 08:14:55 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/z3_model.ML	Wed Nov 17 08:14:56 2010 +0100
     1.3 @@ -115,7 +115,7 @@
     1.4      fun match ts ((n, _), _) = matches terms (member (op aconv) ts) n
     1.5  
     1.6      val (default_int, ints) =
     1.7 -      (case find_first (match [@{term int}]) vs of
     1.8 +      (case find_first (match [@{const of_nat (int)}]) vs of
     1.9          NONE => (NONE, [])
    1.10        | SOME (_, cases) =>
    1.11            let val (cs, (_, e)) = split_last cases
    1.12 @@ -138,7 +138,7 @@
    1.13        | SOME t => ((n, k), map (subst_nat (Term.fastype_of t) k) cases))
    1.14    in
    1.15      map subst_nats vs
    1.16 -    |> filter_out (match [@{term int}, @{term nat}])
    1.17 +    |> filter_out (match [@{const of_nat (int)}, @{const nat}])
    1.18    end
    1.19  
    1.20  fun filter_valid_valuations terms = map_filter (fn
    1.21 @@ -179,8 +179,8 @@
    1.22  
    1.23  fun get_term n (cx as (_, terms, _)) = (the (Symtab.lookup terms n), cx)
    1.24  
    1.25 -fun trans_expr _ True = pair @{term True}
    1.26 -  | trans_expr _ False = pair @{term False}
    1.27 +fun trans_expr _ True = pair @{const True}
    1.28 +  | trans_expr _ False = pair @{const False}
    1.29    | trans_expr T (Number (i, NONE)) = pair (HOLogic.mk_number T i)
    1.30    | trans_expr T (Number (i, SOME j)) =
    1.31        pair (Const (@{const_name divide}, [T, T] ---> T) $