src/Pure/Isar/isar_thy.ML
changeset 7851 4a6df182b093
parent 7775 26898fbd19ca
child 7862 3e75fbd4a46b
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Wed Oct 13 19:40:03 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Wed Oct 13 19:40:23 1999 +0200
     1.3 @@ -457,11 +457,10 @@
     1.4    (Obtain.obtain_i (map Comment.ignore xs) (map Comment.ignore asms));
     1.5  
     1.6  
     1.7 -
     1.8  (* use ML text *)
     1.9  
    1.10 -fun use_mltext txt verb opt_thy = Context.setmp opt_thy (use_text verb) txt;
    1.11 -fun use_mltext_theory txt verb thy = #2 (Context.pass_theory thy (use_text verb) txt);
    1.12 +fun use_mltext txt verb opt_thy = Context.setmp opt_thy (use_text writeln verb) txt;
    1.13 +fun use_mltext_theory txt verb thy = #2 (Context.pass_theory thy (use_text writeln verb) txt);
    1.14  
    1.15  fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false;
    1.16