equal
deleted
inserted
replaced
89 else SOME (ts'', ctxt |
89 else SOME (ts'', ctxt |
90 |> fold (ProofContext.add_const_constraint o apsnd SOME) secondary_constraints |
90 |> fold (ProofContext.add_const_constraint o apsnd SOME) secondary_constraints |
91 |> mark_passed) |
91 |> mark_passed) |
92 end; |
92 end; |
93 |
93 |
|
94 fun rewrite_liberal thy unchecks t = |
|
95 case try (Pattern.rewrite_term thy unchecks []) t |
|
96 of NONE => NONE |
|
97 | SOME t' => if t aconv t' then NONE else SOME t'; |
|
98 |
94 fun improve_term_uncheck ts ctxt = |
99 fun improve_term_uncheck ts ctxt = |
95 let |
100 let |
96 val thy = ProofContext.theory_of ctxt; |
101 val thy = ProofContext.theory_of ctxt; |
97 val unchecks = (#unchecks o ImprovableSyntax.get) ctxt; |
102 val unchecks = (#unchecks o ImprovableSyntax.get) ctxt; |
98 val ts' = map (Pattern.rewrite_term thy unchecks []) ts; |
103 val ts' = map (rewrite_liberal thy unchecks) ts; |
99 in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end; |
104 in if exists is_some ts' then SOME (map2 the_default ts ts', ctxt) else NONE end; |
100 |
105 |
101 fun set_primary_constraints ctxt = |
106 fun set_primary_constraints ctxt = |
102 let |
107 let |
103 val { primary_constraints, ... } = ImprovableSyntax.get ctxt; |
108 val { primary_constraints, ... } = ImprovableSyntax.get ctxt; |
104 in fold (ProofContext.add_const_constraint o apsnd SOME) primary_constraints ctxt end; |
109 in fold (ProofContext.add_const_constraint o apsnd SOME) primary_constraints ctxt end; |