src/Tools/isac/Specify/o-model.sml
changeset 60778 41abd196342a
parent 60766 2e0603ca18a4
     1.1 --- a/src/Tools/isac/Specify/o-model.sml	Sun Dec 10 17:35:07 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/o-model.sml	Mon Dec 11 09:24:02 2023 +0100
     1.3 @@ -48,8 +48,6 @@
     1.4    val is_copy_named': string -> bool
     1.5    val is_copy_named_generating: Model_Pattern.single -> bool
     1.6  
     1.7 -  val get_field_term: theory -> single -> m_field * UnparseC.term_as_string
     1.8 -
     1.9  \<^isac_test>\<open>
    1.10    val is_copy_named_generating_idstr: string -> bool
    1.11    val string_of_preoris : preori list -> string
    1.12 @@ -97,10 +95,6 @@
    1.13  val string_of_preoris = (strs2str' o (map (linefeed o preori2str)));
    1.14  \<close>
    1.15  
    1.16 -(* get the first term in ts from ori *)
    1.17 -fun get_field_term thy (_, _, fd, d, ts) =
    1.18 -  (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d,[hd ts]))
    1.19 -
    1.20  
    1.21  (** initialise O_Model **)
    1.22