changeset 29585 | c23295521af5 |
parent 28965 | 1de908189869 |
child 30280 | eb98b49ef835 |
--- a/src/HOLCF/Tools/domain/domain_extender.ML Wed Jan 21 16:51:45 2009 +0100 +++ b/src/HOLCF/Tools/domain/domain_extender.ML Wed Jan 21 18:27:43 2009 +0100 @@ -134,7 +134,7 @@ in theorems_thy |> Sign.add_path (Sign.base_name comp_dnam) - |> (snd o (PureThy.add_thmss [(("rews", List.concat rewss @ take_rews), [])])) + |> (snd o (PureThy.add_thmss [((Binding.name "rews", List.concat rewss @ take_rews), [])])) |> Sign.parent_path end;