src/HOL/Tools/record.ML

       cterm_instantiate
         (map (pairself cert)
           (case rev params of
             [] =>
               (case AList.lookup (op =) (Term.add_frees g []) s of
-                NONE => sys_error "try_param_tac: no such variable"
+                NONE => error "try_param_tac: no such variable"
               | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))])
           | (_, T) :: _ =>
               [(P, list_abs (params, if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
                 (x, list_abs (params, Bound 0))])) rule';
   in compose_tac (false, rule'', nprems_of rule) i end);