--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Aug 16 15:35:47 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Aug 16 15:49:16 2013 +0200
@@ -272,7 +272,7 @@
let
fun build (TU as (T, U)) =
if T = U then
- id_const T
+ HOLogic.id_const T
else
(case TU of
(Type (s, Ts), Type (s', Us)) =>