--- a/src/HOL/IMP/Compiler.thy Fri Nov 25 22:10:51 2011 +0100
+++ b/src/HOL/IMP/Compiler.thy Fri Nov 25 22:21:37 2011 +0100
@@ -17,9 +17,8 @@
*}
abbreviation "isize xs == int (length xs)"
-primrec
- inth :: "'a list => int => 'a" (infixl "!!" 100) where
- inth_Cons: "(x # xs) !! n = (if n = 0 then x else xs !! (n - 1))"
+fun inth :: "'a list \<Rightarrow> int \<Rightarrow> 'a" (infixl "!!" 100) where
+"(x # xs) !! n = (if n = 0 then x else xs !! (n - 1))"
text {*
The only additional lemma we need is indexing over append:
@@ -41,7 +40,7 @@
JMPGE int
type_synonym stack = "val list"
-type_synonym config = "int\<times>state\<times>stack"
+type_synonym config = "int \<times> state \<times> stack"
abbreviation "hd2 xs == hd(tl xs)"
abbreviation "tl2 xs == tl(tl xs)"
--- a/src/HOL/Tools/Function/fun.ML Fri Nov 25 22:10:51 2011 +0100
+++ b/src/HOL/Tools/Function/fun.ML Fri Nov 25 22:21:37 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 22:10:51 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Fri Nov 25 22:21:37 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