add_arities_i;
authorwenzelm
Mon Oct 06 19:13:55 1997 +0200 (1997-10-06)
changeset 37936e807b50b6c1
parent 3792 1ecbaca6560a
child 3794 d543bb9ab896
add_arities_i;
src/HOL/typedef.ML
src/HOLCF/domain/syntax.ML
     1.1 --- a/src/HOL/typedef.ML	Mon Oct 06 19:13:29 1997 +0200
     1.2 +++ b/src/HOL/typedef.ML	Mon Oct 06 19:13:55 1997 +0200
     1.3 @@ -108,7 +108,7 @@
     1.4  
     1.5      thy
     1.6      |> Theory.add_types [(t, tlen, mx)]
     1.7 -    |> Theory.add_arities
     1.8 +    |> Theory.add_arities_i
     1.9       [(tname, replicate tlen logicS, logicS),
    1.10        (tname, replicate tlen termS, termS)]
    1.11      |> Theory.add_consts_i
     2.1 --- a/src/HOLCF/domain/syntax.ML	Mon Oct 06 19:13:29 1997 +0200
     2.2 +++ b/src/HOLCF/domain/syntax.ML	Mon Oct 06 19:13:55 1997 +0200
     2.3 @@ -116,7 +116,7 @@
     2.4    val ctt           = map (calc_syntax funprod) eqs';
     2.5    val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false};
     2.6  in thy'' |> Theory.add_types      thy_types
     2.7 -	 |> Theory.add_arities    thy_arities
     2.8 +	 |> Theory.add_arities_i  thy_arities
     2.9  	 |> add_cur_ops_i (flat(map fst ctt))
    2.10  	 |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
    2.11  	 |> Theory.add_trrules_i (flat(map snd ctt))