# HG changeset patch
# User blanchet
# Date 1398241406 -7200
# Node ID a001337c8d24f60e8192b22921e21f3fe65b7a5e
# Parent  18f50d5f84ef391163848e244d41e9782a6764b9
tuned whitespace

diff -r 18f50d5f84ef -r a001337c8d24 src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Wed Apr 23 09:32:00 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Wed Apr 23 10:23:26 2014 +0200
@@ -707,7 +707,7 @@
 
 fun mk_absT thy repT absT repU =
   let
- val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (repT, repU) Vartab.empty) [];
+    val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (repT, repU) Vartab.empty) [];
   in Term.typ_subst_TVars rho absT end
   handle Type.TYPE_MATCH => raise Term.TYPE ("mk_absT", [repT, absT, repU], []);