| changeset 22921 | 475ff421a6a3 |
| parent 22845 | 5f9138bcb3d7 |
| child 23373 | ead82c82da9e |
--- a/src/HOL/Extraction/Higman.thy Thu May 10 10:21:50 2007 +0200 +++ b/src/HOL/Extraction/Higman.thy Thu May 10 10:22:17 2007 +0200 @@ -333,8 +333,8 @@ *} consts_code - arbitrary :: "LT" ("({* L0 [] [] *})") - arbitrary :: "TT" ("({* T0 A [] [] [] R0 *})") + "arbitrary :: LT" ("({* L0 [] [] *})") + "arbitrary :: TT" ("({* T0 A [] [] [] R0 *})") code_module Higman contains