# HG changeset patch
# User wenzelm
# Date 1392049393 -3600
# Node ID ca31f042414f6471f194d35e59ef7416e8541d0d
# Parent  4de48353034e9892c1a03079d7cc3ce1614465f9
more explicit axiomatization;

diff -r 4de48353034e -r ca31f042414f src/HOL/HOLCF/ex/Focus_ex.thy
--- a/src/HOL/HOLCF/ex/Focus_ex.thy	Mon Feb 10 17:20:11 2014 +0100
+++ b/src/HOL/HOLCF/ex/Focus_ex.thy	Mon Feb 10 17:23:13 2014 +0100
@@ -103,7 +103,8 @@
 begin
 
 typedecl ('a, 'b) tc
-arities tc:: (pcpo, pcpo) pcpo
+axiomatization where tc_arity: "OFCLASS(('a::pcpo, 'b::pcpo) tc, pcop_class)"
+instance tc :: (pcpo, pcpo) pcpo by (rule tc_arity)
 
 axiomatization
   Rf :: "('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool"