equal
deleted
inserted
replaced
89 val _ = null not_defined |
89 val _ = null not_defined |
90 orelse error ("No defining equations for function" ^ |
90 orelse error ("No defining equations for function" ^ |
91 plural " " "s " not_defined ^ commas_quote not_defined) |
91 plural " " "s " not_defined ^ commas_quote not_defined) |
92 |
92 |
93 fun check_sorts ((fname, fT), _) = |
93 fun check_sorts ((fname, fT), _) = |
94 Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, @{sort "pt"}) |
94 Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, @{sort "pt"}) |
95 orelse error (cat_lines |
95 orelse error (cat_lines |
96 ["Type of " ^ quote fname ^ " is not of sort " ^ quote "pt" ^ ":", |
96 ["Type of " ^ quote fname ^ " is not of sort " ^ quote "pt" ^ ":", |
97 Syntax.string_of_typ (Config.put show_sorts true ctxt) fT]) |
97 Syntax.string_of_typ (Config.put show_sorts true ctxt) fT]) |
98 |
98 |
99 val _ = map check_sorts fixes |
99 val _ = map check_sorts fixes |
182 fs=fs, R=R, defname=defname, is_partial=true, eqvts=eqvts} |
182 fs=fs, R=R, defname=defname, is_partial=true, eqvts=eqvts} |
183 |
183 |
184 val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes) |
184 val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes) |
185 in |
185 in |
186 (info, |
186 (info, |
187 lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info)) |
187 lthy |> Local_Theory.declaration {syntax = false, pervasive = false} |
|
188 (add_function_data o morph_function_data info)) |
188 end |
189 end |
189 in |
190 in |
190 ((goal_state, afterqed), lthy') |
191 ((goal_state, afterqed), lthy') |
191 end |
192 end |
192 |
193 |