# HG changeset patch
# User berghofe
# Date 1086094826 -7200
# Node ID e9e0d8618043876f7070293754a4972e77027ebb
# Parent  b4be6bdcbb94f530d4f140beed2fff36d0f295c5
Adapted to new name mangling function in code generator.

diff -r b4be6bdcbb94 -r e9e0d8618043 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Tue Jun 01 14:59:54 2004 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Tue Jun 01 15:00:26 2004 +0200
@@ -535,10 +535,10 @@
 *}
 
 ML {*
-fun nat_of_int 0 = id0
+fun nat_of_int 0 = id_0
   | nat_of_int n = Suc (nat_of_int (n-1));
 
-fun int_of_nat id0 = 0
+fun int_of_nat id_0 = 0
   | int_of_nat (Suc n) = 1 + int_of_nat n;
 
 fun dBtype_of_typ (Type ("fun", [T, U])) =
@@ -576,7 +576,7 @@
       let val dBT = dBtype_of_typ T
       in rtypingT_Abs (e, dBT, dB_of_term t,
         dBtype_of_typ (fastype_of1 (T :: Ts, t)),
-        typing_of_term (T :: Ts) (shift e id0 dBT) t)
+        typing_of_term (T :: Ts) (shift e id_0 dBT) t)
       end
   | typing_of_term _ _ _ = error "typing_of_term: bad term";