# HG changeset patch
# User krauss
# Date 1158746731 -7200
# Node ID 241792a4634eee9f7e8a764795f1a645ed9ea2c8
# Parent  d883e0fc1c51c7372633c272eea3d2ca1d53972a
Removed "induct set" attribute from total induction rules

diff -r d883e0fc1c51 -r 241792a4634e src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Sep 20 10:13:36 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Sep 20 12:05:31 2006 +0200
@@ -135,7 +135,7 @@
         lthy
           |> add_simps "simps" [] mutual_info fixes tsimps stmts
           |> with_local_path defname
-                (LocalTheory.note (("induct", [Attrib.internal (InductAttrib.induct_set "")]), tinduct) #> snd)
+                (LocalTheory.note (("induct", []), tinduct) #> snd)
     end