src/HOLCF/domain/syntax.ML
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 *)