src/HOL/Tools/Metis/metis_reconstruct.ML
changeset 43297 e77baf329f48
parent 43294 0271fda2a83a
parent 43278 1fbdcebb364b
child 43298 82d4874757df
equal deleted inserted replaced
43296:755e3d5ea3f2 43297:e77baf329f48
   375                 val (tm1, args) = strip_comb tm
   375                 val (tm1, args) = strip_comb tm
   376                 val adjustment = length ts - length args
   376                 val adjustment = length ts - length args
   377                 val p' = if adjustment > p then p else p - adjustment
   377                 val p' = if adjustment > p then p else p - adjustment
   378                 val tm_p =
   378                 val tm_p =
   379                   nth args p'
   379                   nth args p'
   380                   handle Subscript => path_finder_fail tm (p :: ps) (SOME t)
   380                   handle General.Subscript => path_finder_fail tm (p :: ps) (SOME t)
   381                 val _ = trace_msg ctxt (fn () =>
   381                 val _ = trace_msg ctxt (fn () =>
   382                     "path_finder: " ^ string_of_int p ^ "  " ^
   382                     "path_finder: " ^ string_of_int p ^ "  " ^
   383                     Syntax.string_of_term ctxt tm_p)
   383                     Syntax.string_of_term ctxt tm_p)
   384                 val (r, t) = path_finder tm_p ps (nth ts p)
   384                 val (r, t) = path_finder tm_p ps (nth ts p)
   385               in (r, list_comb (tm1, replace_item_list t p' args)) end
   385               in (r, list_comb (tm1, replace_item_list t p' args)) end