equal
deleted
inserted
replaced
8 signature ERROR_PATTERN_DEFINITION = |
8 signature ERROR_PATTERN_DEFINITION = |
9 sig |
9 sig |
10 eqtype id |
10 eqtype id |
11 type T = id * term list * thm list |
11 type T = id * term list * thm list |
12 val s_to_string : T list -> string |
12 val s_to_string : T list -> string |
|
13 val adapt_to_type: Proof.context -> T -> T |
13 |
14 |
14 type fill_in_id |
15 type fill_in_id |
15 type fill_in |
16 type fill_in |
16 end |
17 end |
17 |
18 |
30 fillpatterns are stored with these thms. *) |
31 fillpatterns are stored with these thms. *) |
31 fun errpat2str (id, tms, thms) = |
32 fun errpat2str (id, tms, thms) = |
32 "(\"" ^ id ^ "\",\n" ^ UnparseC.terms tms ^ ",\n" ^ ThmC_Def.string_of_thms thms |
33 "(\"" ^ id ^ "\",\n" ^ UnparseC.terms tms ^ ",\n" ^ ThmC_Def.string_of_thms thms |
33 fun s_to_string errpats = (strs2str' o (map errpat2str)) errpats |
34 fun s_to_string errpats = (strs2str' o (map errpat2str)) errpats |
34 |
35 |
|
36 fun adapt_to_type ctxt (id, terms, thms) = |
|
37 (id, map (Model_Pattern.adapt_term_to_type ctxt) terms, thms) |
|
38 |
35 (* for (at least) 2 kinds of access: |
39 (* for (at least) 2 kinds of access: |
36 (1) given an id, find the respective fill_in's (e.g. in fun find_fill_patterns) |
40 (1) given an id, find the respective fill_in's (e.g. in fun find_fill_patterns) |
37 (2) given a thm, find respective fill_in's *) |
41 (2) given a thm, find respective fill_in's *) |
38 type fill_in_id = string |
42 type fill_in_id = string |
39 type fill_in = |
43 type fill_in = |