src/HOLCF/domain/syntax.ML
changeset 3771 ede66fb99880
parent 3534 c245c88194ff
child 3793 6e807b50b6c1
     1.1 --- a/src/HOLCF/domain/syntax.ML	Wed Oct 01 18:19:44 1997 +0200
     1.2 +++ b/src/HOLCF/domain/syntax.ML	Thu Oct 02 22:54:00 1997 +0200
     1.3 @@ -115,11 +115,11 @@
     1.4    val const_bisim  = (comp_dname^"_bisim" ,relprod --> HOLogic.boolT, NoSyn');
     1.5    val ctt           = map (calc_syntax funprod) eqs';
     1.6    val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false};
     1.7 -in thy'' |> add_types      thy_types
     1.8 -	 |> add_arities    thy_arities
     1.9 +in thy'' |> Theory.add_types      thy_types
    1.10 +	 |> Theory.add_arities    thy_arities
    1.11  	 |> add_cur_ops_i (flat(map fst ctt))
    1.12  	 |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
    1.13 -	 |> add_trrules_i (flat(map snd ctt))
    1.14 +	 |> Theory.add_trrules_i (flat(map snd ctt))
    1.15  end; (* let *)
    1.16  
    1.17  end; (* local *)