1.1 --- a/src/Tools/isac/BaseDefinitions/substitution.sml	Wed Oct 19 14:23:40 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/substitution.sml	Wed Oct 19 15:39:15 2022 +0200
     1.3 @@ -27,7 +27,6 @@
     1.4    val T_from_string_eqs: theory -> as_string_eqs -> T
     1.5    val T_from_input: Proof.context -> input -> T
     1.6  
     1.7 -  val input_to_terms: Proof.context -> input -> as_eqs
     1.8    val eqs_to_input: as_eqs -> as_string_eqs
     1.9    val program_to_input: program -> input
    1.10    val for_bdv: program -> T -> input option * T
    1.11 @@ -79,11 +78,6 @@
    1.12  
    1.13  val eqs_to_input = map UnparseC.term;
    1.14  
    1.15 -(* TermC.parse ctxt fails with "c_2 = 0" \<longrightarrow> \<open>c_2 = (0 :: 'a)\<close> and thus requires adapt_to_type *)
    1.16 -fun input_to_terms ctxt strs = strs
    1.17 -  |> map (TermC.parse ctxt)
    1.18 -  |> map (Model_Pattern.adapt_term_to_type ctxt)
    1.19 -
    1.20  fun program_to_input sub = (sub 
    1.21    |> HOLogic.dest_list 
    1.22    |> map HOLogic.dest_prod