changeset 16850 | 35e07087aba2 |
parent 16790 | be2780f435e1 |
child 16861 | 7446b4be013b |
--- a/src/Pure/Isar/locale.ML Thu Jul 14 19:28:33 2005 +0200 +++ b/src/Pure/Isar/locale.ML Thu Jul 14 19:28:34 2005 +0200 @@ -1983,7 +1983,7 @@ val tinst = Symtab.make (map (fn ((x, 0), T) => (x, T |> renameT) - | ((_, n), _) => error "Internal error var in prep_registration") vinst); + | ((_, n), _) => sys_error "Internal error var in prep_registration") vinst); val inst = Symtab.make (given_ps ~~ map rename vs); (* defined params without user input *)