changeset 22796 | 34c316d7b630 |
parent 19092 | e32cf29f01fc |
--- a/src/HOLCF/domain/syntax.ML Thu Apr 26 12:00:01 2007 +0200 +++ b/src/HOLCF/domain/syntax.ML Thu Apr 26 12:00:05 2007 +0200 @@ -144,7 +144,7 @@ in thy'' |> ContConsts.add_consts_i (List.concat (map fst ctt) @ (if length eqs'>1 then [const_copy] else[])@ [const_bisim]) - |> Theory.add_trrules_i (List.concat(map snd ctt)) + |> Sign.add_trrules_i (List.concat(map snd ctt)) end; (* let *) end; (* local *)