--- a/src/HOL/Lambda/ListOrder.thy Wed Oct 18 23:40:58 2000 +0200
+++ b/src/HOL/Lambda/ListOrder.thy Wed Oct 18 23:41:28 2000 +0200
@@ -6,7 +6,7 @@
header {* Lifting an order to lists of elements *}
-theory ListOrder = Acc:
+theory ListOrder = Accessible_Part:
text {*
Lifting an order to lists of elements, relating exactly one
--- a/src/HOL/Lambda/ROOT.ML Wed Oct 18 23:40:58 2000 +0200
+++ b/src/HOL/Lambda/ROOT.ML Wed Oct 18 23:41:28 2000 +0200
@@ -5,5 +5,5 @@
*)
time_use_thy "Eta";
-with_path "../Induct" time_use_thy "Acc";
+time_use_thy "Accessible_Part";
time_use_thy "Type";