# HG changeset patch
# User traytel
# Date 1393936682 -3600
# Node ID 21aa30ea680644e240fdbd6c3621806c687a4688
# Parent  8c0a13e84963f5d1a501d160520011e37ab91e1d
propagate the exception that is expected later on

diff -r 8c0a13e84963 -r 21aa30ea6806 src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Tue Mar 04 12:32:33 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Tue Mar 04 13:38:02 2014 +0100
@@ -627,8 +627,10 @@
    type_definition = Morphism.thm phi type_definition};
 
 fun mk_absT thy repT absT repU =
-  let val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (repT, repU) Vartab.empty) [];
-  in Term.typ_subst_TVars rho absT end;
+  let
+ 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], []);
 
 fun mk_repT absT repT absU =
   if absT = repT then absU