--- a/src/HOL/Fun.thy Thu Mar 15 20:07:00 2012 +0100 +++ b/src/HOL/Fun.thy Thu Mar 15 22:08:53 2012 +0100 @@ -7,6 +7,7 @@ theory Fun imports Complete_Lattices +keywords "enriched_type" :: thy_goal uses ("Tools/enriched_type.ML") begin