1.1 --- a/src/HOL/Tools/refute.ML	Fri Mar 10 12:28:38 2006 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Fri Mar 10 15:33:48 2006 +0100
     1.3 @@ -622,9 +622,9 @@
     1.4  			| Const ("Finite_Set.card", T)    => collect_type_axioms (axs, T)
     1.5  			| Const ("Finite_Set.Finites", T) => collect_type_axioms (axs, T)
     1.6  			| Const ("op <", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => collect_type_axioms (axs, T)
     1.7 -			| Const ("op +", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
     1.8 -			| Const ("op -", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
     1.9 -			| Const ("op *", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
    1.10 +			| Const ("HOL.plus", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
    1.11 +			| Const ("HOL.minus", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
    1.12 +			| Const ("HOL.times", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
    1.13  			| Const ("List.op @", T)          => collect_type_axioms (axs, T)
    1.14  			| Const ("Lfp.lfp", T)            => collect_type_axioms (axs, T)
    1.15  			| Const ("Gfp.gfp", T)            => collect_type_axioms (axs, T)
    1.16 @@ -2162,13 +2162,13 @@
    1.17  
    1.18  	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
    1.19  
    1.20 -	(* only an optimization: 'op +' could in principle be interpreted with    *)
    1.21 +	(* only an optimization: 'HOL.plus' could in principle be interpreted with*)
    1.22  	(* interpreters available already (using its definition), but the code    *)
    1.23  	(* below is more efficient                                                *)
    1.24  
    1.25  	fun Nat_plus_interpreter thy model args t =
    1.26  		case t of
    1.27 -		  Const ("op +", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
    1.28 +		  Const ("HOL.plus", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
    1.29  			let
    1.30  				val (i_nat, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
    1.31  				val size_nat      = size_of_type i_nat
    1.32 @@ -2196,7 +2196,7 @@
    1.33  
    1.34  	fun Nat_minus_interpreter thy model args t =
    1.35  		case t of
    1.36 -		  Const ("op -", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
    1.37 +		  Const ("HOL.minus", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
    1.38  			let
    1.39  				val (i_nat, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
    1.40  				val size_nat      = size_of_type i_nat
    1.41 @@ -2215,13 +2215,13 @@
    1.42  
    1.43  	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
    1.44  
    1.45 -	(* only an optimization: 'op *' could in principle be interpreted with    *)
    1.46 -	(* interpreters available already (using its definition), but the code    *)
    1.47 -	(* below is more efficient                                                *)
    1.48 +	(* only an optimization: 'HOL.times' could in principle be interpreted with *)
    1.49 +	(* interpreters available already (using its definition), but the code      *)
    1.50 +	(* below is more efficient                                                  *)
    1.51  
    1.52  	fun Nat_mult_interpreter thy model args t =
    1.53  		case t of
    1.54 -		  Const ("op *", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
    1.55 +		  Const ("HOL.times", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
    1.56  			let
    1.57  				val (i_nat, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
    1.58  				val size_nat      = size_of_type i_nat