Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/function_package/fundef_package.ML
changeset 20638 241792a4634e
parent 20523 36a59e5d0039
child 20654 d80502f0d701 
--- 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
isabelle