1.1 --- a/src/Tools/isac/Specify/p-model.sml	Sat Feb 04 16:49:08 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/p-model.sml	Sat Feb 04 17:00:25 2023 +0100
     1.3 @@ -65,11 +65,11 @@
     1.4  
     1.5  (*val item_to_out: Proof.context -> I_Model.single -> out_element*)
     1.6  fun item_to_out ctxt (_, _, _, _, I_Model.Cor (dsc_ts, _)) =
     1.7 -    (dsc_ts |> Term.list_comb |> UnparseC.term_in_ctxt ctxt, Cor)
     1.8 +    (dsc_ts |> Term.list_comb |> UnparseC.term ctxt, Cor)
     1.9    | item_to_out ctxt (_, _, _, _, I_Model.Inc (dsc_ts, _)) =
    1.10 -    (dsc_ts |> Term.list_comb |> UnparseC.term_in_ctxt ctxt, Inc)
    1.11 +    (dsc_ts |> Term.list_comb |> UnparseC.term ctxt, Inc)
    1.12    | item_to_out ctxt ((_, _, _, _, I_Model.Sup dsc_ts): I_Model.single) =
    1.13 -    (dsc_ts |> Term.list_comb |> UnparseC.term_in_ctxt ctxt, Sup)
    1.14 +    (dsc_ts |> Term.list_comb |> UnparseC.term ctxt, Sup)
    1.15    | item_to_out ctxt im =
    1.16      raise ERROR ("P_Model.item_to_out called with " ^ I_Model.single_to_string ctxt im)
    1.17  
    1.18 @@ -80,7 +80,7 @@
    1.19  
    1.20  (*val where_to_out: Proof.context -> bool * term -> out_element*)
    1.21  fun where_to_out ctxt (bool, t) =
    1.22 -  (UnparseC.term_in_ctxt ctxt t, if bool then True else False)
    1.23 +  (UnparseC.term ctxt t, if bool then True else False)
    1.24  
    1.25  (*val wheres_to_out: Proof.context -> (bool * term) list -> field_out*)
    1.26  fun wheres_to_out ctxt wheres = ("#Where", map (where_to_out ctxt) wheres)
    1.27 @@ -171,8 +171,8 @@
    1.28  fun add_where {Given = gi, Where = _, Find = fi, With = wi, Relate = re} wh =
    1.29    {Given = gi, Where = wh, Find= fi , With = wi, Relate = re}
    1.30  
    1.31 -fun boolterm2item ctxt (true, term) = Correct (UnparseC.term_in_ctxt ctxt term)
    1.32 -  | boolterm2item ctxt(false, term) = False (UnparseC.term_in_ctxt ctxt term);
    1.33 +fun boolterm2item ctxt (true, term) = Correct (UnparseC.term ctxt term)
    1.34 +  | boolterm2item ctxt(false, term) = False (UnparseC.term ctxt term);
    1.35  
    1.36  fun from thy itms where_ =
    1.37    let