src/HOL/Tools/SMT/smtlib_interface.ML
changeset 66134 a1fb6beb2731
parent 59058 a78612c67ec0
child 66551 4df6b0ae900d
     1.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Jun 20 08:01:56 2017 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Jun 20 14:33:45 2017 +0200
     1.3 @@ -94,8 +94,6 @@
     1.4    | tree_of_sterm _ (SMT_Translate.SApp (n, [])) = SMTLIB.Sym n
     1.5    | tree_of_sterm l (SMT_Translate.SApp (n, ts)) =
     1.6        SMTLIB.S (SMTLIB.Sym n :: map (tree_of_sterm l) ts)
     1.7 -  | tree_of_sterm _ (SMT_Translate.SLet _) =
     1.8 -      raise Fail "SMT-LIB: unsupported let expression"
     1.9    | tree_of_sterm l (SMT_Translate.SQua (q, ss, pats, t)) =
    1.10        let
    1.11          val l' = l + length ss