# HG changeset patch
# User haftmann
# Date 1163428992 -3600
# Node ID caa210551c01021aad3d5af713c4ae18c5c22622
# Parent  eb291029d6cd5a0374d6d77899f241cc6d486a67
adjusted name in generated code

diff -r eb291029d6cd -r caa210551c01 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Mon Nov 13 15:43:11 2006 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy	Mon Nov 13 15:43:12 2006 +0100
@@ -624,13 +624,13 @@
 fun typing_of_term Ts e (Bound i) =
       Norm.Var (e, nat_of_int i, dBtype_of_typ (nth Ts i))
   | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of
-        Type ("fun", [T, U]) => Norm.App_1 (e, dB_of_term t,
+        Type ("fun", [T, U]) => Norm.Appa (e, dB_of_term t,
           dBtype_of_typ T, dBtype_of_typ U, dB_of_term u,
           typing_of_term Ts e t, typing_of_term Ts e u)
       | _ => error "typing_of_term: function type expected")
   | typing_of_term Ts e (Abs (s, T, t)) =
       let val dBT = dBtype_of_typ T
-      in Norm.Abs_1 (e, dBT, dB_of_term t,
+      in Norm.Absa (e, dBT, dB_of_term t,
         dBtype_of_typ (fastype_of1 (T :: Ts, t)),
         typing_of_term (T :: Ts) (Type.shift e ROOT.Nat.Zero_nat dBT) t)
       end