# HG changeset patch
# User haftmann
# Date 1292939663 -3600
# Node ID 57ebe94c7fbfc6c570e2c72479bacb3ca7e205a9
# Parent  3cb30e525ee9320ba7860bb5c1ae1f6cd46b9350
renamed mk_id to the more canonical id_const

diff -r 3cb30e525ee9 -r 57ebe94c7fbf src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Tue Dec 21 14:18:45 2010 +0100
+++ b/src/HOL/Tools/hologic.ML	Tue Dec 21 14:54:23 2010 +0100
@@ -8,7 +8,7 @@
 sig
   val typeS: sort
   val typeT: typ
-  val mk_id: typ -> term
+  val id_const: typ -> term
   val mk_comp: term * term -> term
   val boolN: string
   val boolT: typ
@@ -146,7 +146,7 @@
 
 (* functions *)
 
-fun mk_id T = Const ("Fun.id", T --> T);
+fun id_const T = Const ("Fun.id", T --> T);
 
 fun mk_comp (f, g) =
   let