--- a/src/HOL/Tools/refute.ML Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/refute.ML Thu Jan 28 11:48:49 2010 +0100
@@ -708,13 +708,13 @@
(* other optimizations *)
| Const (@{const_name Finite_Set.card}, _) => t
| Const (@{const_name Finite_Set.finite}, _) => t
- | Const (@{const_name HOL.less}, Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Algebras.less}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
- | Const (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Algebras.plus}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
- | Const (@{const_name HOL.minus}, Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Algebras.minus}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
- | Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Algebras.times}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
| Const (@{const_name List.append}, _) => t
| Const (@{const_name lfp}, _) => t
@@ -883,16 +883,16 @@
| Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs
| Const (@{const_name Finite_Set.finite}, T) =>
collect_type_axioms T axs
- | Const (@{const_name HOL.less}, T as Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Algebras.less}, T as Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
collect_type_axioms T axs
- | Const (@{const_name HOL.plus}, T as Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Algebras.plus}, T as Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
collect_type_axioms T axs
- | Const (@{const_name HOL.minus}, T as Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Algebras.minus}, T as Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
collect_type_axioms T axs
- | Const (@{const_name HOL.times}, T as Type ("fun", [Type ("nat", []),
+ | Const (@{const_name Algebras.times}, T as Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
collect_type_axioms T axs
| Const (@{const_name List.append}, T) => collect_type_axioms T axs
@@ -2765,13 +2765,13 @@
(* theory -> model -> arguments -> Term.term ->
(interpretation * model * arguments) option *)
- (* only an optimization: 'HOL.less' could in principle be interpreted with *)
+ (* only an optimization: 'less' could in principle be interpreted with *)
(* interpreters available already (using its definition), but the code *)
(* below is more efficient *)
fun Nat_less_interpreter thy model args t =
case t of
- Const (@{const_name HOL.less}, Type ("fun", [Type ("nat", []),
+ Const (@{const_name Algebras.less}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
let
val size_of_nat = size_of_type thy model (Type ("nat", []))
@@ -2788,13 +2788,13 @@
(* theory -> model -> arguments -> Term.term ->
(interpretation * model * arguments) option *)
- (* only an optimization: 'HOL.plus' could in principle be interpreted with *)
+ (* only an optimization: 'plus' could in principle be interpreted with *)
(* interpreters available already (using its definition), but the code *)
(* below is more efficient *)
fun Nat_plus_interpreter thy model args t =
case t of
- Const (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []),
+ Const (@{const_name Algebras.plus}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
let
val size_of_nat = size_of_type thy model (Type ("nat", []))
@@ -2819,13 +2819,13 @@
(* theory -> model -> arguments -> Term.term ->
(interpretation * model * arguments) option *)
- (* only an optimization: 'HOL.minus' could in principle be interpreted *)
+ (* only an optimization: 'minus' could in principle be interpreted *)
(* with interpreters available already (using its definition), but the *)
(* code below is more efficient *)
fun Nat_minus_interpreter thy model args t =
case t of
- Const (@{const_name HOL.minus}, Type ("fun", [Type ("nat", []),
+ Const (@{const_name Algebras.minus}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
let
val size_of_nat = size_of_type thy model (Type ("nat", []))
@@ -2847,13 +2847,13 @@
(* theory -> model -> arguments -> Term.term ->
(interpretation * model * arguments) option *)
- (* only an optimization: 'HOL.times' could in principle be interpreted *)
+ (* only an optimization: 'times' could in principle be interpreted *)
(* with interpreters available already (using its definition), but the *)
(* code below is more efficient *)
fun Nat_times_interpreter thy model args t =
case t of
- Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []),
+ Const (@{const_name Algebras.times}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
let
val size_of_nat = size_of_type thy model (Type ("nat", []))