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 Nov 25 19:07:26 2011 +0100 (2011-11-25)
changeset 45639efddd75c741e
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
src/HOL/Tools/Quickcheck/quickcheck_common.ML
     1.1 --- a/src/HOL/Tools/Function/fun.ML	Fri Nov 25 12:18:39 2011 +0100
     1.2 +++ b/src/HOL/Tools/Function/fun.ML	Fri Nov 25 19:07:26 2011 +0100
     1.3 @@ -161,7 +161,6 @@
     1.4    in
     1.5      lthy
     1.6      |> add pat_completeness_auto |> snd
     1.7 -    |> Local_Theory.restore
     1.8      |> prove_termination |> snd
     1.9    end
    1.10  
     2.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Fri Nov 25 12:18:39 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Fri Nov 25 19:07:26 2011 +0100
     2.3 @@ -309,7 +309,6 @@
     2.4          (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs_t)
     2.5          Function_Common.default_config pat_completeness_auto
     2.6        #> snd
     2.7 -      #> Local_Theory.restore
     2.8        #> (fn lthy => Function.prove_termination NONE (the termination_tac lthy) lthy)
     2.9        #> snd
    2.10      end