--- a/src/HOL/Matrix/Compute_Oracle/linker.ML Fri Sep 24 15:14:55 2010 +0200
+++ b/src/HOL/Matrix/Compute_Oracle/linker.ML Fri Sep 24 15:30:30 2010 +0200
@@ -166,7 +166,7 @@
else case Consttab.lookup insttab constant of
SOME _ => instantiations
| NONE => ((constant', (constant, Sign.typ_match thy (ty', ty) empty_subst))::instantiations
- handle TYPE_MATCH => instantiations))
+ handle Type.TYPE_MATCH => instantiations))
ctab instantiations
val instantiations = fold calc_instantiations cs []
(*val _ = writeln ("instantiations = "^(makestring (length instantiations)))*)