equal
deleted
inserted
replaced
251 in |
251 in |
252 lthy |
252 lthy |
253 |> set_group ? LocalTheory.set_group (serial_string ()) |
253 |> set_group ? LocalTheory.set_group (serial_string ()) |
254 |> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs |
254 |> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs |
255 |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec')) |
255 |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec')) |
256 |-> (fn simps => fold_map (LocalTheory.note Thm.generated_theoremK) simps) |
256 |-> (fn simps => fold_map (LocalTheory.note Thm.generatedK) simps) |
257 |-> (fn simps' => LocalTheory.note Thm.generated_theoremK |
257 |-> (fn simps' => LocalTheory.note Thm.generatedK |
258 ((qualify (Binding.qualified_name "simps"), simp_atts), maps snd simps')) |
258 ((qualify (Binding.qualified_name "simps"), simp_atts), maps snd simps')) |
259 |>> snd |
259 |>> snd |
260 end handle PrimrecError (msg, some_eqn) => |
260 end handle PrimrecError (msg, some_eqn) => |
261 error ("Primrec definition error:\n" ^ msg ^ (case some_eqn |
261 error ("Primrec definition error:\n" ^ msg ^ (case some_eqn |
262 of SOME eqn => "\nin\n" ^ quote (Syntax.string_of_term lthy eqn) |
262 of SOME eqn => "\nin\n" ^ quote (Syntax.string_of_term lthy eqn) |