src/Pure/Interface/proof_general.ML
changeset 9050 578730810638
parent 9010 ce78dc5e1a73
child 9462 3ac87f80186d
equal deleted inserted replaced
9049:8a3101b62c4f 9050:578730810638
   140 
   140 
   141 
   141 
   142 (* prepare theory context *)
   142 (* prepare theory context *)
   143 
   143 
   144 val thy_name = Path.pack o Path.drop_ext o Path.base o Path.unpack;
   144 val thy_name = Path.pack o Path.drop_ext o Path.base o Path.unpack;
   145 val update_thy_only = ThyInfo.update_thy_only;
   145 val update_thy_only = setmp Thm.trace_simp false ThyInfo.update_thy_only;
   146 
   146 
   147 fun which_context () =
   147 fun which_context () =
   148   (case Context.get_context () of
   148   (case Context.get_context () of
   149     Some thy => "  Using current (dynamic!) one: " ^
   149     Some thy => "  Using current (dynamic!) one: " ^
   150       (case try PureThy.get_name thy of Some name => quote name | None => "<unnamed>")
   150       (case try PureThy.get_name thy of Some name => quote name | None => "<unnamed>")