Theory.inferT_axm;

--- a/src/HOLCF/domain/axioms.ML	Sat Apr 14 17:36:01 2007 +0200
+++ b/src/HOLCF/domain/axioms.ML	Sat Apr 14 17:36:03 2007 +0200
@@ -14,7 +14,7 @@
 infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<;
 infix 9 `   ; infix 9 `% ; infix 9 `%%; infixr 9 oo;
 
-fun infer_types thy' = map (inferT_axm thy');
+fun infer_types thy' = map (Theory.inferT_axm thy');
 
 fun calc_axioms comp_dname (eqs : eq list) n (((dname,_),cons) : eq)=
 let

--- a/src/HOLCF/fixrec_package.ML	Sat Apr 14 17:36:01 2007 +0200
+++ b/src/HOLCF/fixrec_package.ML	Sat Apr 14 17:36:03 2007 +0200
@@ -91,7 +91,7 @@
       | defs (l::ls) r = one_def l (%%:"Cprod.cfst"`r) :: defs ls (%%:"Cprod.csnd"`r);
     val (names, pre_fixdefs) = ListPair.unzip (defs lhss fixpoint);
     
-    val fixdefs = map (inferT_axm thy) pre_fixdefs;
+    val fixdefs = map (Theory.inferT_axm thy) pre_fixdefs;
     val (fixdef_thms, thy') =
       PureThy.add_defs_i false (map Thm.no_attributes fixdefs) thy;
     val ctuple_fixdef_thm = foldr1 (fn (x,y) => cpair_equalI OF [x,y]) fixdef_thms;