src/HOL/Tools/BNF/bnf_comp.ML
changeset 56634 a001337c8d24
parent 56254 a2dd9200854d
child 57567 d554b0097ad4
--- 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], []);