# HG changeset patch
# User wenzelm
# Date 1176564963 -7200
# Node ID b11a9beabe7d91f277f7ff233c8f89fe1442a27e
# Parent  522f4f8aa2970adb8aeaca696e575152bd821d24
Theory.inferT_axm;

diff -r 522f4f8aa297 -r b11a9beabe7d src/HOLCF/domain/axioms.ML
--- 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
diff -r 522f4f8aa297 -r b11a9beabe7d src/HOLCF/fixrec_package.ML
--- 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;