diff -r 294b5905f4eb -r ede66fb99880 src/HOLCF/domain/syntax.ML
--- a/src/HOLCF/domain/syntax.ML	Wed Oct 01 18:19:44 1997 +0200
+++ b/src/HOLCF/domain/syntax.ML	Thu Oct 02 22:54:00 1997 +0200
@@ -115,11 +115,11 @@
   val const_bisim  = (comp_dname^"_bisim" ,relprod --> HOLogic.boolT, NoSyn');
   val ctt           = map (calc_syntax funprod) eqs';
   val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false};
-in thy'' |> add_types      thy_types
-	 |> add_arities    thy_arities
+in thy'' |> Theory.add_types      thy_types
+	 |> Theory.add_arities    thy_arities
 	 |> add_cur_ops_i (flat(map fst ctt))
 	 |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
-	 |> add_trrules_i (flat(map snd ctt))
+	 |> Theory.add_trrules_i (flat(map snd ctt))
 end; (* let *)
 
 end; (* local *)