Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
propagate the exception that is expected later on
authortraytel
Tue, 04 Mar 2014 13:38:02 +0100
changeset 55900 21aa30ea6806
parent 55899 8c0a13e84963
child 55901 8c6d49dd8ae1
propagate the exception that is expected later on
src/HOL/Tools/BNF/bnf_comp.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle