# HG changeset patch
# User nipkow
# Date 1322219913 -3600
# Node ID 5f85efcb50c19b77925f07d36b5784dd02beb91c
# Parent  f21eb7073895be7816a47c8befe431898ddef360
tuned

diff -r f21eb7073895 -r 5f85efcb50c1 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Fri Nov 25 00:18:59 2011 +0000
+++ b/src/HOL/IMP/Compiler.thy	Fri Nov 25 12:18:33 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)"