# HG changeset patch
# User haftmann
# Date 1174647943 -3600
# Node ID 04242efdcece146dfcb8eb06c28b4a76417ecb14
# Parent  ca326e0fb5c50a7685755ac798f512c064875306
fixed typing bug in generated code

diff -r ca326e0fb5c5 -r 04242efdcece src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Fri Mar 23 10:50:03 2007 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy	Fri Mar 23 12:05:43 2007 +0100
@@ -6,7 +6,9 @@
 
 header {* Weak normalization for simply-typed lambda calculus *}
 
-theory WeakNorm imports Type begin
+theory WeakNorm
+imports Type
+begin
 
 text {*
 Formalization by Stefan Berghofer. Partly based on a paper proof by
@@ -554,15 +556,11 @@
 *}
 
 ML {*
-val thy = the_context ();
-fun rd s = read_cterm thy (s, TypeInfer.logicT);
-
-val ct1 = rd "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))";
+val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
 val (dB1, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct1));
 val ct1' = cterm_of thy (term_of_dB [] (#T (rep_cterm ct1)) dB1);
 
-val ct2 = rd
-  "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))";
+val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"};
 val (dB2, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2));
 val ct2' = cterm_of thy (term_of_dB [] (#T (rep_cterm ct2)) dB2);
 *}
@@ -584,8 +582,8 @@
 structure Lambda = ROOT.Lambda;
 structure Nat = ROOT.Nat;
 
-val nat_of_int = ROOT.Integer.nat;
-val int_of_nat = ROOT.Integer.int;
+val nat_of_int = ROOT.Integer.nat o IntInf.fromInt;
+val int_of_nat = IntInf.toInt o ROOT.Integer.int;
 
 fun dBtype_of_typ (Type ("fun", [T, U])) =
       Type.Fun (dBtype_of_typ T, dBtype_of_typ U)
@@ -630,13 +628,12 @@
 *}
 
 ML {*
-val ct1 = rd "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))";
+val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
 val (dB1, _) = ROOT.WeakNorm.type_NF (typing_of_term [] dummyf (term_of ct1));
 val ct1' = cterm_of thy (term_of_dB [] (#T (rep_cterm ct1)) dB1);
 
-val ct2 = rd
-  "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))";
-val (dB2, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2));
+val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"};
+val (dB2, _) = ROOT.WeakNorm.type_NF (typing_of_term [] dummyf (term_of ct2));
 val ct2' = cterm_of thy (term_of_dB [] (#T (rep_cterm ct2)) dB2);
 *}