restore instead of init
authorhaftmann
Fri, 14 Mar 2008 12:18:56 +0100
changeset 26270 73ac6430f5e7
parent 26269 5bb50f58a113
child 26271 e324f8918c98
restore instead of init
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;