src/HOL/Tools/Metis/metis_reconstruct.ML
changeset 43297 e77baf329f48
parent 43294 0271fda2a83a
parent 43278 1fbdcebb364b
child 43298 82d4874757df
--- 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)