# HG changeset patch
# User blanchet
# Date 1449004900 -3600
# Node ID 2cd36f4c5d6554309bbbfe371e9a77bee5a65a0e
# Parent  99f1eaf70c3dc640699a5d1d441195a8c7d1c685
tuned whitespace

diff -r 99f1eaf70c3d -r 2cd36f4c5d65 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Tue Dec 01 22:21:37 2015 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML	Tue Dec 01 22:21:40 2015 +0100
@@ -385,19 +385,18 @@
 fun specialize_type thy (s, T) t =
   let
     fun subst_for (Const (s', T')) =
-      if s = s' then
-        SOME (Sign.typ_match thy (T', T) Vartab.empty)
-        handle Type.TYPE_MATCH => NONE
-      else
-        NONE
-    | subst_for (t1 $ t2) =
-      (case subst_for t1 of SOME x => SOME x | NONE => subst_for t2)
-    | subst_for (Abs (_, _, t')) = subst_for t'
-    | subst_for _ = NONE
+        if s = s' then
+          SOME (Sign.typ_match thy (T', T) Vartab.empty)
+          handle Type.TYPE_MATCH => NONE
+        else
+          NONE
+      | subst_for (t1 $ t2) = (case subst_for t1 of SOME x => SOME x | NONE => subst_for t2)
+      | subst_for (Abs (_, _, t')) = subst_for t'
+      | subst_for _ = NONE
   in
-    case subst_for t of
+    (case subst_for t of
       SOME subst => monomorphic_term subst t
-    | NONE => raise Type.TYPE_MATCH
+    | NONE => raise Type.TYPE_MATCH)
   end
 
 fun strip_subgoal goal i ctxt =