src/HOL/Tools/res_clause.ML
changeset 23881 851c74f1bb69
parent 23385 0ef4f9fc0d09
child 24183 a46b758941a4
     1.1 --- a/src/HOL/Tools/res_clause.ML	Fri Jul 20 14:28:05 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Fri Jul 20 14:28:25 2007 +0200
     1.3 @@ -89,8 +89,8 @@
     1.4  (*Provide readable names for the more common symbolic functions*)
     1.5  val const_trans_table =
     1.6        Symtab.make [("op =", "equal"),
     1.7 -	  	   (@{const_name Orderings.less_eq}, "lessequals"),
     1.8 -		   (@{const_name Orderings.less}, "less"),
     1.9 +	  	   (@{const_name HOL.less_eq}, "lessequals"),
    1.10 +		   (@{const_name HOL.less}, "less"),
    1.11  		   ("op &", "and"),
    1.12  		   ("op |", "or"),
    1.13  		   (@{const_name HOL.plus}, "plus"),