--- a/src/HOL/Tools/hologic.ML Tue Mar 26 12:20:56 2013 +0100 +++ b/src/HOL/Tools/hologic.ML Tue Mar 26 12:20:56 2013 +0100 @@ -572,7 +572,7 @@ (* real *) -val realT = Type ("RealDef.real", []); +val realT = Type ("Real.real", []); (* list *)