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)