# HG changeset patch
# User krauss
# Date 1322244446 -3600
# Node ID efddd75c741e6acfcf4036806c66d608f5604cc5
# Parent  e5fd20f232412bc3ff8de7ca252d8c81edd41cda
removed obsolete uses of Local_Theory.restore -- package composition P1 #> P2 no longer requires them due to 57def0b39696: P2 finds the results of P1 in the auxiliary context

diff -r e5fd20f23241 -r efddd75c741e src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Fri Nov 25 12:18:39 2011 +0100
+++ b/src/HOL/Tools/Function/fun.ML	Fri Nov 25 19:07:26 2011 +0100
@@ -161,7 +161,6 @@
   in
     lthy
     |> add pat_completeness_auto |> snd
-    |> Local_Theory.restore
     |> prove_termination |> snd
   end
 
diff -r e5fd20f23241 -r efddd75c741e src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Fri Nov 25 12:18:39 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Fri Nov 25 19:07:26 2011 +0100
@@ -309,7 +309,6 @@
         (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs_t)
         Function_Common.default_config pat_completeness_auto
       #> snd
-      #> Local_Theory.restore
       #> (fn lthy => Function.prove_termination NONE (the termination_tac lthy) lthy)
       #> snd
     end