equal
deleted
inserted
replaced
34 val is_copy_named_idstr: string -> bool |
34 val is_copy_named_idstr: string -> bool |
35 val is_copy_named_generating_idstr: string -> bool |
35 val is_copy_named_generating_idstr: string -> bool |
36 val is_copy_named_generating: Model_Pattern.single -> bool |
36 val is_copy_named_generating: Model_Pattern.single -> bool |
37 |
37 |
38 val preoris2str : preori list -> string |
38 val preoris2str : preori list -> string |
|
39 val getr_ct: theory -> single -> m_field * UnparseC.term_as_string |
|
40 |
39 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
41 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
40 val add_field: theory -> Model_Pattern.T -> term * 'b -> m_field * descriptor * 'b |
42 val add_field: theory -> Model_Pattern.T -> term * 'b -> m_field * descriptor * 'b |
41 val add_variants: ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list |
43 val add_variants: ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list |
42 val max: variants -> int |
44 val max: variants -> int |
43 val coll_variants: ('a * ''b) list -> ('a list * ''b) list |
45 val coll_variants: ('a * ''b) list -> ('a list * ''b) list |
68 type preori = (variants * m_field * term * term list); |
70 type preori = (variants * m_field * term * term list); |
69 fun preori2str (vs, fi, t, ts) = |
71 fun preori2str (vs, fi, t, ts) = |
70 "(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^ |
72 "(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^ |
71 UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")"; |
73 UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")"; |
72 val preoris2str = (strs2str' o (map (linefeed o preori2str))); |
74 val preoris2str = (strs2str' o (map (linefeed o preori2str))); |
|
75 |
|
76 (* get the first term in ts from ori *) |
|
77 fun getr_ct thy (_, _, fd, d, ts) = |
|
78 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d,[hd ts])) |
73 |
79 |
74 |
80 |
75 (** initialise O_Model **) |
81 (** initialise O_Model **) |
76 |
82 |
77 (* compare d and dsc in pbt and transfer field to pre-ori *) |
83 (* compare d and dsc in pbt and transfer field to pre-ori *) |