--- a/src/HOL/Tools/record.ML Wed Nov 03 10:48:55 2010 +0100
+++ b/src/HOL/Tools/record.ML Wed Nov 03 10:51:40 2010 +0100
@@ -1578,7 +1578,7 @@
(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)))),