equal
deleted
inserted
replaced
162 let |
162 let |
163 val ctxt0 = Proof_Context.init_global thy; |
163 val ctxt0 = Proof_Context.init_global thy; |
164 val ctxt = |
164 val ctxt = |
165 (case opt_src of |
165 (case opt_src of |
166 NONE => ctxt0 |
166 NONE => ctxt0 |
167 | SOME src => #2 (Method.syntax (Method.sections recdef_modifiers) src ctxt0)); |
167 | SOME src => #2 (Args.syntax (Method.sections recdef_modifiers) src ctxt0)); |
168 val {simps, congs, wfs} = get_hints ctxt; |
168 val {simps, congs, wfs} = get_hints ctxt; |
169 val ctxt' = ctxt addsimps simps |> Simplifier.del_cong @{thm imp_cong}; |
169 val ctxt' = ctxt addsimps simps |> Simplifier.del_cong @{thm imp_cong}; |
170 in (ctxt', rev (map snd congs), wfs) end; |
170 in (ctxt', rev (map snd congs), wfs) end; |
171 |
171 |
172 fun prepare_hints_i thy () = |
172 fun prepare_hints_i thy () = |