src/ZF/Inductive_ZF.thy

--- a/src/ZF/Inductive_ZF.thy	Wed Aug 18 12:08:21 2010 +0200
+++ b/src/ZF/Inductive_ZF.thy	Wed Aug 18 12:19:27 2010 +0200
@@ -31,8 +31,8 @@
 lemma refl_thin: "!!P. a = a ==> P ==> P" .
 
 use "ind_syntax.ML"
+use "Tools/ind_cases.ML"
 use "Tools/cartprod.ML"
-use "Tools/ind_cases.ML"
 use "Tools/inductive_package.ML"
 use "Tools/induct_tacs.ML"
 use "Tools/primrec_package.ML"