src/HOL/Matrix/Compute_Oracle/linker.ML

                               if free <> free' orelse name <> name' then
                                   instantiations
                               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)))*)
         fun update_ctab (constant', entry) ctab =
             (case Consttab.lookup ctab constant' of