src/Pure/Isar/isar_thy.ML
changeset 6266 a5f9fa6b6d7c
parent 6253 dbaf79ac2ff9
child 6331 fb7b8d6c2bd1
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Mon Feb 08 17:33:24 1999 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Mon Feb 08 17:33:47 1999 +0100
     1.3 @@ -174,24 +174,8 @@
     1.4  
     1.5  (* use ML text *)
     1.6  
     1.7 -fun use_mltext txt opt_thy =
     1.8 -  let
     1.9 -    val save_context = Context.get_context ();
    1.10 -    val _ = Context.set_context opt_thy;
    1.11 -    val opt_exn = (transform_error (use_text false) txt; None) handle exn => Some exn;
    1.12 -    val opt_thy' = Context.get_context ();
    1.13 -  in
    1.14 -    Context.set_context save_context;
    1.15 -    (case opt_exn of
    1.16 -      None => opt_thy'
    1.17 -    | Some exn => raise exn)
    1.18 -  end;
    1.19 -
    1.20 -fun use_mltext_theory txt thy =
    1.21 -  (case use_mltext txt (Some thy) of
    1.22 -    Some thy' => thy'
    1.23 -  | None => error "Missing result ML theory context");
    1.24 -
    1.25 +fun use_mltext txt opt_thy = #2 (Context.fetch opt_thy (use_text false) txt);
    1.26 +fun use_mltext_theory txt thy = #2 (Context.fetch_theory thy (use_text false) txt);
    1.27  
    1.28  fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");");
    1.29  
    1.30 @@ -241,8 +225,10 @@
    1.31  (* theory init and exit *)
    1.32  
    1.33  fun begin_theory (name, parents, files) () =
    1.34 -  let val thy = ThyInfo.begin_theory name parents
    1.35 -  in seq ThyInfo.use (mapfilter (fn (x, true) => Some x | _ => None) files); thy end;
    1.36 +  let
    1.37 +    val thy = ThyInfo.begin_theory name parents;
    1.38 +    val names = mapfilter (fn (x, true) => Some x | _ => None) files;
    1.39 +  in Context.setmp (Some thy) (seq ThyInfo.use) names; thy end;
    1.40  
    1.41  fun end_theory thy =
    1.42    let val thy' = PureThy.end_theory thy in