# HG changeset patch
# User haftmann
# Date 1205493536 -3600
# Node ID 73ac6430f5e73bffdc36d3fda5bf9068e5bf1777
# Parent  5bb50f58a1135af99c3a24f5a4297dab3adba2c2
restore instead of init

diff -r 5bb50f58a113 -r 73ac6430f5e7 src/HOL/Tools/function_package/fundef_datatype.ML
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Mar 14 08:52:55 2008 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Mar 14 12:18:56 2008 +0100
@@ -309,7 +309,7 @@
       |> LocalTheory.set_group group
       |> FundefPackage.add_fundef fixes statements config flags
       |> by_pat_completeness_simp
-      |> LocalTheory.reinit
+      |> LocalTheory.restore
       |> LocalTheory.set_group group
       |> termination_by_lexicographic_order
   end;