
diff -r 33ab01218ae1 -r bd9c4e8281ec 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"




