81 | _ => error "fun T_from_string_eqs"; |
81 | _ => error "fun T_from_string_eqs"; |
82 |
82 |
83 "-------- fun input_to_terms -------------------------------------------------"; |
83 "-------- fun input_to_terms -------------------------------------------------"; |
84 "-------- fun input_to_terms -------------------------------------------------"; |
84 "-------- fun input_to_terms -------------------------------------------------"; |
85 "-------- fun input_to_terms -------------------------------------------------"; |
85 "-------- fun input_to_terms -------------------------------------------------"; |
86 Subst.input_to_terms: Subst.input -> term list; |
|
87 val input = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(aaa, bbb + 2)"]; |
86 val input = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(aaa, bbb + 2)"]; |
88 |
87 |
89 case Subst.input_to_terms input of |
88 case Subst.input_to_terms @{context} input of |
90 [Const (\<^const_name>\<open>Pair\<close>, _) $ |
89 [Const (\<^const_name>\<open>Pair\<close>, _) $ |
91 (Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>Char\<close>, _) $ |
90 (Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>Char\<close>, _) $ |
92 Const (\<^const_name>\<open>False\<close>, _) $ _ $ _ $ _ $ _ $ _ $ _ $ _) $ _) $ |
91 Const (\<^const_name>\<open>False\<close>, _) $ _ $ _ $ _ $ _ $ _ $ _ $ _) $ _) $ |
93 Free ("x", _), |
92 Free ("x", _), |
94 _, |
93 _, |