equal
deleted
inserted
replaced
112 let val {primary_constraints, ...} = Improvable_Syntax.get ctxt; |
112 let val {primary_constraints, ...} = Improvable_Syntax.get ctxt; |
113 in fold (Proof_Context.add_const_constraint o apsnd SOME) primary_constraints ctxt end; |
113 in fold (Proof_Context.add_const_constraint o apsnd SOME) primary_constraints ctxt end; |
114 |
114 |
115 val activate_improvable_syntax = |
115 val activate_improvable_syntax = |
116 Context.proof_map |
116 Context.proof_map |
117 (Syntax_Phases.context_term_check 0 "improvement" improve_term_check |
117 (Syntax_Phases.term_check' 0 "improvement" improve_term_check |
118 #> Syntax_Phases.context_term_uncheck 0 "improvement" improve_term_uncheck) |
118 #> Syntax_Phases.term_uncheck' 0 "improvement" improve_term_uncheck) |
119 #> set_primary_constraints; |
119 #> set_primary_constraints; |
120 |
120 |
121 |
121 |
122 (* overloading target *) |
122 (* overloading target *) |
123 |
123 |