# HG changeset patch
# User wenzelm
# Date 1226954208 -3600
# Node ID b3ce1912ac258cfb73213d3dd689470b68230fce
# Parent  3b460b6eadae14a7550a00f7abcd5b9999623712
removed Induct/Mutil.thy -- the file has been moved to AFP;

diff -r 3b460b6eadae -r b3ce1912ac25 src/HOL/Induct/ROOT.ML
--- a/src/HOL/Induct/ROOT.ML	Mon Nov 17 21:28:46 2008 +0100
+++ b/src/HOL/Induct/ROOT.ML	Mon Nov 17 21:36:48 2008 +0100
@@ -4,6 +4,6 @@
 setmp_noncritical quick_and_dirty true
   use_thy "Common_Patterns";
 
-use_thys ["Mutil", "QuoDataType", "QuoNestedDataType", "Term",
+use_thys ["QuoDataType", "QuoNestedDataType", "Term",
   "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog",
   "SList", "LFilter", "Com"];