src/HOL/Tools/refute.ML
changeset 19277 f7602e74d948
parent 19233 77ca20b0ed77
child 19346 c4c003abd830
     1.1 --- a/src/HOL/Tools/refute.ML	Thu Mar 16 20:19:25 2006 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Fri Mar 17 09:34:23 2006 +0100
     1.3 @@ -621,7 +621,7 @@
     1.4  			(* other optimizations *)
     1.5  			| Const ("Finite_Set.card", T)    => collect_type_axioms (axs, T)
     1.6  			| Const ("Finite_Set.Finites", T) => collect_type_axioms (axs, T)
     1.7 -			| Const ("op <", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => collect_type_axioms (axs, T)
     1.8 +			| Const ("Orderings.less", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => collect_type_axioms (axs, T)
     1.9  			| Const ("HOL.plus", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
    1.10  			| Const ("HOL.minus", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
    1.11  			| Const ("HOL.times", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
    1.12 @@ -2146,7 +2146,7 @@
    1.13  
    1.14  	fun Nat_less_interpreter thy model args t =
    1.15  		case t of
    1.16 -		  Const ("op <", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
    1.17 +		  Const ("Orderings.less", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
    1.18  			let
    1.19  				val (i_nat, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
    1.20  				val size_nat      = size_of_type i_nat