# HG changeset patch
# User wenzelm
# Date 1313055625 -7200
# Node ID f3058e539e3a6ea3ab4786c4ab9dc73e5a25fd3f
# Parent  8bc84fa57a13fc85fe2b4f0d3817943f747be2fe
redundant use of misc_legacy.ML;

diff -r 8bc84fa57a13 -r f3058e539e3a src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Thu Aug 11 10:36:34 2011 +0200
+++ b/src/ZF/IsaMakefile	Thu Aug 11 11:40:25 2011 +0200
@@ -27,19 +27,18 @@
 FOL:
 	@cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL
 
-$(OUT)/ZF: $(OUT)/FOL $(SRC)/Tools/misc_legacy.ML AC.thy Arith.thy	\
-  ArithSimp.thy Bin.thy Bool.thy Cardinal.thy CardinalArith.thy		\
-  Cardinal_AC.thy Datatype_ZF.thy Epsilon.thy EquivClass.thy		\
-  Finite.thy Fixedpt.thy Inductive_ZF.thy InfDatatype.thy Int_ZF.thy	\
-  IntArith.thy IntDiv_ZF.thy List_ZF.thy Main.thy Main_ZF.thy		\
-  Main_ZFC.thy Nat_ZF.thy OrdQuant.thy Order.thy OrderArith.thy		\
-  OrderType.thy Ordinal.thy Perm.thy QPair.thy QUniv.thy ROOT.ML	\
-  Sum.thy Tools/cartprod.ML Tools/datatype_package.ML			\
-  Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML	\
-  Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML	\
-  Trancl.thy Univ.thy WF.thy ZF.thy Zorn.thy arith_data.ML		\
-  equalities.thy func.thy ind_syntax.ML int_arith.ML pair.thy		\
-  simpdata.ML upair.thy
+$(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy ArithSimp.thy Bin.thy Bool.thy	\
+  Cardinal.thy CardinalArith.thy Cardinal_AC.thy Datatype_ZF.thy	\
+  Epsilon.thy EquivClass.thy Finite.thy Fixedpt.thy Inductive_ZF.thy	\
+  InfDatatype.thy Int_ZF.thy IntArith.thy IntDiv_ZF.thy List_ZF.thy	\
+  Main.thy Main_ZF.thy Main_ZFC.thy Nat_ZF.thy OrdQuant.thy Order.thy	\
+  OrderArith.thy OrderType.thy Ordinal.thy Perm.thy QPair.thy		\
+  QUniv.thy ROOT.ML Sum.thy Tools/cartprod.ML				\
+  Tools/datatype_package.ML Tools/ind_cases.ML Tools/induct_tacs.ML	\
+  Tools/inductive_package.ML Tools/numeral_syntax.ML			\
+  Tools/primrec_package.ML Tools/typechk.ML Trancl.thy Univ.thy WF.thy	\
+  ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy ind_syntax.ML	\
+  int_arith.ML pair.thy simpdata.ML upair.thy
 	@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/FOL ZF
 
 
diff -r 8bc84fa57a13 -r f3058e539e3a src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Thu Aug 11 10:36:34 2011 +0200
+++ b/src/ZF/ZF.thy	Thu Aug 11 11:40:25 2011 +0200
@@ -7,7 +7,6 @@
 
 theory ZF
 imports FOL
-uses "~~/src/Tools/misc_legacy.ML"
 begin
 
 declare [[eta_contract = false]]