# HG changeset patch
# User haftmann
# Date 1160469282 -7200
# Node ID 43e216a9d615a544dd1348cad2989697c839f4ac
# Parent  beedcae49096c169a52ff345ebff991717868d96
purged some ML legacy

diff -r beedcae49096 -r 43e216a9d615 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Tue Oct 10 10:34:41 2006 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Tue Oct 10 10:34:42 2006 +0200
@@ -566,17 +566,17 @@
 *}
 
 ML {*
-val sg = sign_of (the_context());
-fun rd s = read_cterm sg (s, TypeInfer.logicT);
+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 (dB1, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct1));
-val ct1' = cterm_of sg (term_of_dB [] (#T (rep_cterm ct1)) dB1);
+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_of sg (term_of_dB [] (#T (rep_cterm ct2)) dB2);
+val ct2' = cterm_of thy (term_of_dB [] (#T (rep_cterm ct2)) dB2);
 *}
 
 end