src/HOL/Tools/SMT/smt_real.ML
changeset 40516 516a367eb38c
parent 38715 6513ea67d95d
child 40579 98ebd2300823
     1.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Fri Nov 12 15:56:10 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Fri Nov 12 15:56:11 2010 +0100
     1.3 @@ -78,7 +78,8 @@
     1.4  local
     1.5    structure I = Z3_Interface
     1.6  
     1.7 -  fun z3_mk_builtin_typ (I.Sym ("real", _)) = SOME @{typ real}
     1.8 +  fun z3_mk_builtin_typ (I.Sym ("Real", _)) = SOME @{typ real}
     1.9 +    | z3_mk_builtin_typ (I.Sym ("real", _)) = SOME @{typ real} (*FIXME: delete*)
    1.10      | z3_mk_builtin_typ _ = NONE
    1.11  
    1.12    fun z3_mk_builtin_num _ i T =