diff -r 755e3d5ea3f2 -r e77baf329f48 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Jun 08 17:01:07 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Jun 08 22:13:49 2011 +0200
@@ -377,7 +377,7 @@
                 val p' = if adjustment > p then p else p - adjustment
                 val tm_p =
                   nth args p'
-                  handle Subscript => path_finder_fail tm (p :: ps) (SOME t)
+                  handle General.Subscript => path_finder_fail tm (p :: ps) (SOME t)
                 val _ = trace_msg ctxt (fn () =>
                     "path_finder: " ^ string_of_int p ^ "  " ^
                     Syntax.string_of_term ctxt tm_p)