| changeset 22677 | b11a9beabe7d |
| parent 22578 | b0eb5652f210 |
| child 22706 | d4696154264f |
--- 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