equal
deleted
inserted
replaced
1071 |> numbers_to_string (*TODO drop*) |
1071 |> numbers_to_string (*TODO drop*) |
1072 |> typ_a2real; (*TODO drop*) |
1072 |> typ_a2real; (*TODO drop*) |
1073 |
1073 |
1074 (*version for testing local to theories*) |
1074 (*version for testing local to theories*) |
1075 fun str2term_ thy str = (term_of o the o (parse thy)) str; |
1075 fun str2term_ thy str = (term_of o the o (parse thy)) str; |
1076 fun str2term str = (term_of o the o (parse (Thy_Info.get_theory "Isac"))) str; |
1076 (*WN110520 |
|
1077 fun str2term str = (term_of o the o (parse (Thy_Info.get_theory "Isac"))) str;*) |
|
1078 fun str2term str = parse_patt (Thy_Info.get_theory "Isac") str |
1077 fun strs2terms ss = map str2term ss; |
1079 fun strs2terms ss = map str2term ss; |
1078 fun str2termN str = (term_of o the o (parseN (Thy_Info.get_theory "Isac"))) str; |
1080 fun str2termN str = (term_of o the o (parseN (Thy_Info.get_theory "Isac"))) str; |
1079 |
1081 |
1080 (*+ makes a substitution from the output of Pattern.match +*) |
1082 (*+ makes a substitution from the output of Pattern.match +*) |
1081 (*fun mk_subs ((id, _):indexname, t:term) = (Free (id,type_of t), t);*) |
1083 (*fun mk_subs ((id, _):indexname, t:term) = (Free (id,type_of t), t);*) |