# HG changeset patch
# User nipkow
# Date 1322219919 -3600
# Node ID e5fd20f232412bc3ff8de7ca252d8c81edd41cda
# Parent  ef08425dd2d5c72fae6eddb72f2deb0ed48848c7# Parent  5f85efcb50c19b77925f07d36b5784dd02beb91c
merged

diff -r ef08425dd2d5 -r e5fd20f23241 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Fri Nov 25 10:52:30 2011 +0100
+++ b/src/HOL/IMP/Compiler.thy	Fri Nov 25 12:18:39 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)"