src/Pure/Tools/plugin.ML
changeset 58665 50b229a5a097
parent 58660 8d4aebb9e327
child 58666 9e3426766267
     1.1 --- a/src/Pure/Tools/plugin.ML	Mon Oct 13 20:51:48 2014 +0200
     1.2 +++ b/src/Pure/Tools/plugin.ML	Mon Oct 13 21:41:29 2014 +0200
     1.3 @@ -163,10 +163,8 @@
     1.4    unfinished_data #> (fn (unfinished, thy) =>
     1.5      if forall (null o #2) unfinished then NONE
     1.6      else
     1.7 -      Named_Target.theory_init thy
     1.8 -      |> fold_rev (fn (interp, data) => fold_rev (apply true interp) data) unfinished
     1.9 -      |> Local_Theory.exit_global
    1.10 -      |> SOME);
    1.11 +      SOME (Named_Target.theory_map
    1.12 +        (fold_rev (fn (interp, data) => fold_rev (apply true interp) data) unfinished) thy));
    1.13  
    1.14  end;
    1.15