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_datatype.ML
changeset 25289 3d332d8a827c
parent 25222 78943ac46f6d
child 25361 1aa441e48496 
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Nov 05 20:50:41 2007 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Nov 05 20:50:42 2007 +0100
@@ -306,7 +306,7 @@
     lthy
       |> FundefPackage.add_fundef fixes statements config flags
       |> by_pat_completeness_simp
-      |> (fn lthy => LocalTheory.reinit lthy (ProofContext.theory_of lthy))
+      |> LocalTheory.reinit
       |> termination_by_lexicographic_order
 
 val _ =
isabelle