# HG changeset patch
# User wenzelm
# Date 966257389 -7200
# Node ID f6669dead969a99b10dc9b30d828b834d4eff949
# Parent  f0e811a54254648ef6ef86f892c6e94225a076e3
use_let: exclude 'val';

diff -r f0e811a54254 -r f6669dead969 src/Pure/context.ML
--- a/src/Pure/context.ML	Mon Aug 14 14:48:07 2000 +0200
+++ b/src/Pure/context.ML	Mon Aug 14 14:49:49 2000 +0200
@@ -69,16 +69,16 @@
 
 (* use ML text *)
 
-fun use_mltext txt verb opt_thy = setmp opt_thy (use_text writeln verb) txt;
+fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_text writeln verb txt) ();
 fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_text writeln verb) txt);
 
 fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false;
 
-fun use_let name body txt =
-  use_context ("let val " ^ name ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
+fun use_let bind body txt =
+  use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
 
 val use_setup =
-  use_let "setup: (theory -> theory) list" "Library.apply setup";
+  use_let "val setup: (theory -> theory) list" "Library.apply setup";
 
 
 end;