1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Mon Feb 03 15:19:07 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Mon Feb 03 15:33:18 2014 +0100
     1.3 @@ -41,12 +41,12 @@
     1.4    post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd
     1.5  
     1.6  fun fold_map_atypes f T s =
     1.7 -  case T of
     1.8 +  (case T of
     1.9      Type (name, Ts) =>
    1.10 -        let val (Ts, s) = fold_map (fold_map_atypes f) Ts s in
    1.11 -          (Type (name, Ts), s)
    1.12 -        end
    1.13 -  | _ => f T s
    1.14 +    let val (Ts, s) = fold_map (fold_map_atypes f) Ts s in
    1.15 +      (Type (name, Ts), s)
    1.16 +    end
    1.17 +  | _ => f T s)
    1.18  
    1.19  val indexname_ord = Term_Ord.fast_indexname_ord
    1.20  val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)