--- a/src/HOL/IsaMakefile Fri Dec 09 14:22:05 2011 +0100
+++ b/src/HOL/IsaMakefile Fri Dec 09 14:46:18 2011 +0100
@@ -1508,7 +1508,8 @@
Quotient_Examples/DList.thy Quotient_Examples/Quotient_Cset.thy \
Quotient_Examples/FSet.thy Quotient_Examples/List_Quotient_Cset.thy \
Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy \
- Quotient_Examples/Lift_Set.thy Quotient_Examples/Lift_RBT.thy
+ Quotient_Examples/Lift_Set.thy Quotient_Examples/Lift_RBT.thy \
+ Quotient_Examples/Lift_Fun.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
--- a/src/HOL/Quotient_Examples/ROOT.ML Fri Dec 09 14:22:05 2011 +0100
+++ b/src/HOL/Quotient_Examples/ROOT.ML Fri Dec 09 14:46:18 2011 +0100
@@ -5,5 +5,5 @@
*)
use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset",
- "List_Quotient_Cset", "Lift_Set", "Lift_RBT"];
+ "List_Quotient_Cset", "Lift_Set", "Lift_RBT", "Lift_Fun"];