1.1 --- a/src/Tools/isac/BaseDefinitions/substitution.sml	Sun Oct 09 09:01:29 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/substitution.sml	Wed Oct 19 10:43:04 2022 +0200
     1.3 @@ -27,7 +27,7 @@
     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: input -> term list
     1.8 +  val input_to_terms: Proof.context -> input -> as_eqs
     1.9    val eqs_to_input: as_eqs -> as_string_eqs
    1.10    val program_to_input: program -> input
    1.11    val for_bdv: program -> T -> input option * T
    1.12 @@ -78,8 +78,11 @@
    1.13    handle TERM _ => raise TERM ("T_from_input: wrong argument " ^ strs2str' input, [])
    1.14  
    1.15  val eqs_to_input = map UnparseC.term;
    1.16 -(*TODO: input requires parse _: _ -> _ option*)
    1.17 -val input_to_terms = map TermC.str2term;
    1.18 +
    1.19 +(* TermC.parse ctxt fails with "c_2 = 0" \<longrightarrow> \<open>c_2 = (0 :: 'a)\<close> and thus requires adapt_to_type *)
    1.20 +fun input_to_terms ctxt strs = strs
    1.21 +  |> map (TermC.parse ctxt)
    1.22 +  |> map (Model_Pattern.adapt_term_to_type ctxt)
    1.23  
    1.24  fun program_to_input sub = (sub 
    1.25    |> HOLogic.dest_list