equal
deleted
inserted
replaced
294 val names1 = map snd fnames; |
294 val names1 = map snd fnames; |
295 val names2 = map fst rec_eqns; |
295 val names2 = map fst rec_eqns; |
296 val primrec_name = |
296 val primrec_name = |
297 if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name; |
297 if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name; |
298 val (thy', defs_thms') = thy |> Theory.add_path primrec_name |> |
298 val (thy', defs_thms') = thy |> Theory.add_path primrec_name |> |
299 (if eq_set (names1, names2) then (PureThy.add_defs_i o map Thm.no_attributes) defs' |
299 (if eq_set (names1, names2) then (PureThy.add_defs_i false o map Thm.no_attributes) defs' |
300 else primrec_err ("functions " ^ commas_quote names2 ^ |
300 else primrec_err ("functions " ^ commas_quote names2 ^ |
301 "\nare not mutually recursive")); |
301 "\nare not mutually recursive")); |
302 val rewrites = o_def :: (map mk_meta_eq rec_rewrites) @ defs_thms'; |
302 val rewrites = o_def :: (map mk_meta_eq rec_rewrites) @ defs_thms'; |
303 val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names1 ^ " ..."); |
303 val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names1 ^ " ..."); |
304 val simps = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (Theory.sign_of thy') t) |
304 val simps = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (Theory.sign_of thy') t) |