Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use_let: exclude 'val';
authorwenzelm
Mon, 14 Aug 2000 14:49:49 +0200
changeset 9586 f6669dead969
parent 9585 f0e811a54254
child 9587 1368ce019457
use_let: exclude 'val';
src/Pure/context.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle