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

diff -r 04242efdcece -r 651777b8dc30 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Fri Mar 23 12:05:43 2007 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy	Fri Mar 23 12:06:41 2007 +0100
@@ -558,11 +558,11 @@
 ML {*
 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 ct1' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct1)) dB1);
 
 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);
+val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
 *}
 
 text {*
@@ -630,11 +630,11 @@
 ML {*
 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 ct1' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct1)) dB1);
 
 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);
+val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
 *}
 
 end