# HG changeset patch
# User wenzelm
# Date 876158035 -7200
# Node ID 6e807b50b6c14f110251a3bb16a2e1ed9a5e775a
# Parent  1ecbaca6560a36d3de6ce758251abcd27523247d
add_arities_i;

diff -r 1ecbaca6560a -r 6e807b50b6c1 src/HOL/typedef.ML
--- a/src/HOL/typedef.ML	Mon Oct 06 19:13:29 1997 +0200
+++ b/src/HOL/typedef.ML	Mon Oct 06 19:13:55 1997 +0200
@@ -108,7 +108,7 @@
 
     thy
     |> Theory.add_types [(t, tlen, mx)]
-    |> Theory.add_arities
+    |> Theory.add_arities_i
      [(tname, replicate tlen logicS, logicS),
       (tname, replicate tlen termS, termS)]
     |> Theory.add_consts_i
diff -r 1ecbaca6560a -r 6e807b50b6c1 src/HOLCF/domain/syntax.ML
--- a/src/HOLCF/domain/syntax.ML	Mon Oct 06 19:13:29 1997 +0200
+++ b/src/HOLCF/domain/syntax.ML	Mon Oct 06 19:13:55 1997 +0200
@@ -116,7 +116,7 @@
   val ctt           = map (calc_syntax funprod) eqs';
   val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false};
 in thy'' |> Theory.add_types      thy_types
-	 |> Theory.add_arities    thy_arities
+	 |> Theory.add_arities_i  thy_arities
 	 |> add_cur_ops_i (flat(map fst ctt))
 	 |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
 	 |> Theory.add_trrules_i (flat(map snd ctt))