src/HOL/Tools/res_clause.ML
changeset 22997 d4f3b015b50b
parent 22643 bc3bb8e9594a
child 23029 79ee75dc1e59
     1.1 --- a/src/HOL/Tools/res_clause.ML	Thu May 17 19:49:21 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Thu May 17 19:49:40 2007 +0200
     1.3 @@ -103,15 +103,15 @@
     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 -	  	   ("Orderings.less_eq", "lessequals"),
     1.8 -		   ("Orderings.less", "less"),
     1.9 +	  	   (@{const_name Orderings.less_eq}, "lessequals"),
    1.10 +		   (@{const_name Orderings.less}, "less"),
    1.11  		   ("op &", "and"),
    1.12  		   ("op |", "or"),
    1.13 -		   ("HOL.plus", "plus"),
    1.14 -		   ("HOL.minus", "minus"),
    1.15 -		   ("HOL.times", "times"),
    1.16 -		   ("Divides.div", "div"),
    1.17 -		   ("HOL.divide", "divide"),
    1.18 +		   (@{const_name HOL.plus}, "plus"),
    1.19 +		   (@{const_name HOL.minus}, "minus"),
    1.20 +		   (@{const_name HOL.times}, "times"),
    1.21 +		   (@{const_name Divides.div}, "div"),
    1.22 +		   (@{const_name HOL.divide}, "divide"),
    1.23  		   ("op -->", "implies"),
    1.24  		   ("{}", "emptyset"),
    1.25  		   ("op :", "in"),