Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
authorkrauss
Fri, 25 Nov 2011 19:07:26 +0100
changeset 45639 efddd75c741e
parent 45638 e5fd20f23241
child 45640 f62edaefff41
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
src/HOL/Tools/Function/fun.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Quickcheck/quickcheck_common.ML file | annotate | diff | comparison | revisions 
--- 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
 
--- 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
isabelle