--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Mon Feb 03 15:19:07 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Mon Feb 03 15:33:18 2014 +0100
@@ -41,12 +41,12 @@
post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd
fun fold_map_atypes f T s =
- case T of
+ (case T of
Type (name, Ts) =>
- let val (Ts, s) = fold_map (fold_map_atypes f) Ts s in
- (Type (name, Ts), s)
- end
- | _ => f T s
+ let val (Ts, s) = fold_map (fold_map_atypes f) Ts s in
+ (Type (name, Ts), s)
+ end
+ | _ => f T s)
val indexname_ord = Term_Ord.fast_indexname_ord
val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)