src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
changeset 52555 6811291d1869
parent 52452 2207825d67f3
child 52627 ecb4a858991d
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Mon Jul 08 14:24:36 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Tue Jul 09 18:44:59 2013 +0200
     1.3 @@ -36,6 +36,7 @@
     1.4        val ((u', s'), Type (_, [_, T])) = post_traverse_term_type' f env u s
     1.5        val ((v', s''), _) = post_traverse_term_type' f env v s'
     1.6      in f (u' $ v') T s'' end
     1.7 +    handle Bind => raise Fail "Sledgehammer_Annotate: post_traverse_term_type'"
     1.8  
     1.9  fun post_traverse_term_type f s t =
    1.10    post_traverse_term_type' (fn t => fn T => fn s => (f t T s, T)) [] t s |> fst